∀ {R : Type u_2} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {P : Algebra.Extension R S} (x y : ↥P.ker),
  Algebra.Extension.Cotangent.of (P.ker.toCotangent (x + y)) =
    Algebra.Extension.Cotangent.of (P.ker.toCotangent x) + Algebra.Extension.Cotangent.of (P.ker.toCotangent y)