English
For rings of integers, the norm composition identity holds: norm_K(norm_F x) = norm_K x.
Русский
Для колец целых нормальная композиционная формула: norm_K(norm_F x) = norm_K x.
LaTeX
$$$\operatorname{norm}_K(\operatorname{norm}_F x) = \operatorname{norm}_K x$$$
Lean4
/-- If `L/K` is a finite Galois extension of fields, then, for all `(x : 𝓞 L)` we have that
`x ∣ algebraMap (𝓞 K) (𝓞 L) (norm K x)`. -/
theorem dvd_norm [FiniteDimensional K L] [IsGalois K L] (x : 𝓞 L) : x ∣ algebraMap (𝓞 K) (𝓞 L) (norm K x) := by
classical
have hint : IsIntegral ℤ (∏ σ ∈ univ.erase (AlgEquiv.refl : L ≃ₐ[K] L), σ x) :=
IsIntegral.prod _ (fun σ _ => ((RingOfIntegers.isIntegral_coe x).map σ))
refine ⟨⟨_, hint⟩, ?_⟩
ext
rw [coe_algebraMap_norm K x, norm_eq_prod_automorphisms]
simp [← Finset.mul_prod_erase _ _ (mem_univ AlgEquiv.refl)]
