norm_complex_apply — Mathlib

English

For z ∈ ℂ, the ℝ-norm of z equals the squared complex modulus, i.e., the real norm equals Complex.normSq(z).

Русский

Для z ∈ ℂ нормa над ℝ равна квадрату модуля z, то есть равенство норм Complex.normSq(z).

LaTeX

$$$\\mathrm{Norm}_{\\mathbb{R}}(z) = \\mathrm{normSq}(z)$$$

Lean4

theorem norm_complex_apply (z : ℂ) : Algebra.norm ℝ z = Complex.normSq z :=
  by
  rw [Algebra.norm_eq_matrix_det Complex.basisOneI, Algebra.leftMulMatrix_complex, Matrix.det_fin_two, normSq_apply]
  simp

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