norm_eq_sqrt_sq_add_sq — Mathlib

English

For any z, the modulus equals the root of the sum of squares of its real and imaginary parts: ||z|| = sqrt((Re z)^2 + (Im z)^2).

Русский

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

LaTeX

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

Lean4

theorem norm_eq_sqrt_sq_add_sq (z : ℂ) : ‖z‖ = √(z.re ^ 2 + z.im ^ 2) := by rw [norm_def, normSq_apply, sq, sq]

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