normSq_sub — Mathlib

English

Further instance of normSq_sub: normSq(z - w) = normSq(z) + normSq(w) - 2 Re(z conj w).

Русский

Еще раз формула normSq для разности: normSq(z - w) = normSq(z) + normSq(w) - 2 Re(z conj w).

LaTeX

$$$$\\|z - w\\|^{2} = \\|z\\|^{2} + \\|w\\|^{2} - 2 \\operatorname{Re}(z \\overline{w}).$$$$

Lean4

theorem normSq_sub (z w : K) : normSq (z - w) = normSq z + normSq w - 2 * re (z * conj w) := by
  simp only [normSq_add, sub_eq_add_neg, map_neg, mul_neg, normSq_neg, map_neg]

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