coe_normSq_add — Mathlib

English

For any quaternions a, b, the norm of the sum satisfies normSq(a+b) = normSq(a) + normSq(b) + 2 Re(a conj(b)).

Русский

Для любых квартонионов a и 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 coe_normSq_add : normSq (a + b) = normSq a + a * star b + b * star a + normSq b := by
  simp only [star_add, ← self_mul_star, mul_add, add_mul, add_assoc, add_left_comm]

Похожие утверждения