coe_algebraMap_norm — Mathlib

English

The algebra map between rings of integers respects norms: algebraMap(𝓞K → 𝓞L)(norm_K x) maps to Algebra.norm_K applied to x under the base change.

Русский

Пусть между кольцами целых 𝓞K и 𝓞L есть отображение алгебра, оно сохраняет нормы: algebraMap(𝓞K → 𝓞L)(norm_K x) сопоставляется норме K на x после базового расширения.

LaTeX

$$$(\mathrm{algebraMap}_{\mathcal{O}K \to \mathcal{O}L})(\mathrm{norm}_K x) = \mathrm{Algebra.norm}_K ( (x) )$$$

Lean4

theorem coe_algebraMap_norm (x : 𝓞 L) :
    (algebraMap (𝓞 K) (𝓞 L) (norm K x) : L) = algebraMap K L (Algebra.norm K (x : L)) :=
  rfl

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