sq_norm_sub_sq_re — Mathlib

English

For any complex z, the relation holds: ||z||^2 = (Re z)^2 + (Im z)^2, hence ||z||^2 - (Re z)^2 = (Im z)^2.

Русский

Для любого z верно: ||z||^2 = (Re z)^2 + (Im z)^2, отсюда ||z||^2 - (Re z)^2 = (Im z)^2.

LaTeX

$$$\\forall z \\in \\mathbb{C}, \\|z\\|^{2} - (\\Re z)^{2} = (\\Im z)^{2}$$$

Lean4

@[simp]
theorem sq_norm_sub_sq_re (z : ℂ) : ‖z‖ ^ 2 - z.re ^ 2 = z.im ^ 2 := by
  rw [Complex.sq_norm, normSq_apply, ← sq, ← sq, add_sub_cancel_left]

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