sq_norm_sub_sq_im — Mathlib

English

For any z, the identity ||z||^2 - (Im z)^2 = (Re z)^2 holds, expressing the squared norm as a sum of squares of real and imaginary parts.

Русский

Для любого z выполнено: ||z||^2 - (Im z)^2 = (Re z)^2, что выражает квадрат нормы через квадраты действительной и мнимой частей.

LaTeX

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

Lean4

@[simp]
theorem sq_norm_sub_sq_im (z : ℂ) : ‖z‖ ^ 2 - z.im ^ 2 = z.re ^ 2 := by rw [← sq_norm_sub_sq_re, sub_sub_cancel]

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