∀ (F : Type u_1) (K : Type u_2) [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra F K] [CharZero F]
  [Algebra.IsIntegral F K] (a b : K),
  Algebra.normalizedTraceAux✝ F K (a + b) = Algebra.normalizedTraceAux✝ F K a + Algebra.normalizedTraceAux✝ F K b