norm_algebraMap — Mathlib

English

For x in 𝓞 K, the K-norm of its image in 𝓞 L equals x raised to the degree [K:L].

Русский

Для x ∈ 𝓞 K, норма по K от образа в 𝓞 L равна x в степени [K: L].

LaTeX

$$$\operatorname{norm}_K(\mathrm{algebraMap}_{\mathcal{O}K \to \mathcal{O}L} x) = x^{\operatorname{finrank} K L}$$$

Lean4

theorem norm_algebraMap (x : 𝓞 K) : norm K (algebraMap (𝓞 K) (𝓞 L) x) = x ^ finrank K L := by
  rw [RingOfIntegers.ext_iff, RingOfIntegers.coe_eq_algebraMap, RingOfIntegers.algebraMap_norm_algebraMap,
    Algebra.norm_algebraMap, RingOfIntegers.coe_eq_algebraMap, map_pow]

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