English
Another form of the additive formula: normSq(a+b) = normSq(a) + normSq(b) + 2 Re(a conj(b)).
Русский
Другая форма формулы сложения нормы: normSq(a+b) = normSq(a) + normSq(b) + 2 Re(a conj(b)).
LaTeX
$$normSq(a + b) = normSq(a) + normSq(b) + 2 * (a * star b).re$$
Lean4
theorem normSq_add (a b : ℍ[R]) : normSq (a + b) = normSq a + normSq b + 2 * (a * star b).re :=
calc
normSq (a + b) = normSq a + (a * star b).re + ((b * star a).re + normSq b) := by
simp_rw [normSq_def, star_add, add_mul, mul_add, re_add]
_ = normSq a + normSq b + ((a * star b).re + (b * star a).re) := by abel
_ = normSq a + normSq b + 2 * (a * star b).re := by rw [← re_add, ← star_mul_star a b, self_add_star', re_coe]
