norm_sub_one_sq_eq_of_norm_one — Mathlib

English

For any z with ‖z‖ = 1, the quantity ‖z − 1‖^2 equals 2(1 − Re z).

Русский

Для любого z на единичной окружности (‖z‖ = 1) выполняется ‖z − 1‖^2 = 2(1 − Re z).

LaTeX

$$$\\|z\\| = 1 \\ \\Rightarrow\\ \\|z-1\\|^2 = 2\\,(1-\\Re z)$$$

Lean4

theorem norm_sub_one_sq_eq_of_norm_one {z : ℂ} (hz : ‖z‖ = 1) : ‖z - 1‖ ^ 2 = 2 * (1 - z.re) :=
  by
  have : z.im * z.im = 1 - z.re * z.re :=
    by
    replace hz := sq_eq_one_iff.mpr (.inl hz)
    rw [Complex.sq_norm, normSq_apply] at hz
    linarith
  simp [Complex.sq_norm, normSq_apply, this]
  ring

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