norm_complex_eq — Mathlib

English

The real algebra norm is equal to the monoid hom given by normSq when seen as a real algebra homomorphism on ℂ.

Русский

Реальная алгебраическая норма совпадает с мономорфизмом normSq, рассматриваемым как гомоморфизм моноидов.

LaTeX

$$$\\mathrm{Algebra.norm}_{\\mathbb{R}} = \\mathrm{normSq}^{\\mathrm{toMonoidHom}}$$$

Lean4

theorem norm_complex_eq : Algebra.norm ℝ = normSq.toMonoidHom :=
  MonoidHom.ext Algebra.norm_complex_apply

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