normSq_sub — Mathlib

English

For z,w ∈ ℂ, the squared norm of the difference satisfies |z − w|^2 = |z|^2 + |w|^2 − 2 Re(z conj(w)).

Русский

Для z,w ∈ ℂ, квадрат нормы разности удовлетворяет |z − w|^2 = |z|^2 + |w|^2 − 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 : ℂ) : normSq (z - w) = normSq z + normSq w - 2 * (z * conj w).re :=
  by
  rw [sub_eq_add_neg, normSq_add]
  simp only [RingHom.map_neg, mul_neg, neg_re, normSq_neg]
  ring

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