norm — Mathlib

English

For x in the ring of integers of L, the K-norm of the F-norm of x equals the K-norm of x: norm_K(norm_F(x)) = norm_K(x).

Русский

Для x ∈ 𝓞 L нормa от K применённая к норме от F к x равна норме от K самой x: \N_K(\N_F(x)) = \N_K(x).

LaTeX

$$$\operatorname{norm}_K(\operatorname{norm}_F(x)) = \operatorname{norm}_K(x)$$$

Lean4

/-- `Algebra.norm` as a morphism between the rings of integers. -/
noncomputable def norm : 𝓞 L →* 𝓞 K :=
  RingOfIntegers.restrict_monoidHom ((Algebra.norm K).comp (algebraMap (𝓞 L) L : (𝓞 L) →* L)) fun x =>
    isIntegral_norm K x.2

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