English
If L/K is Galois, the K-norm of x ∈ L equals the product of its images under all K-automorphisms of L, i.e., Aut_K(L).
Русский
Если L/K — Гало расширение, норма K(x) равна произведению образов x под всеми K-автоморфизмами L.
LaTeX
$$$\\mathrm{norm}_K(x) = \\prod_{\\sigma \\in \\mathrm{Aut}_K(L)} \\sigma(x).$$$
Lean4
theorem norm_eq_prod_automorphisms [IsGalois K L] (x : L) : algebraMap K L (norm K x) = ∏ σ : L ≃ₐ[K] L, σ x :=
by
apply FaithfulSMul.algebraMap_injective L (AlgebraicClosure L)
rw [map_prod (algebraMap L (AlgebraicClosure L))]
rw [← Fintype.prod_equiv (Normal.algHomEquivAut K (AlgebraicClosure L) L)]
· rw [← norm_eq_prod_embeddings _ _ x, ← IsScalarTower.algebraMap_apply]
· intro σ
simp only [Normal.algHomEquivAut, AlgHom.restrictNormal', Equiv.coe_fn_mk, AlgEquiv.coe_ofBijective,
AlgHom.restrictNormal_commutes, algebraMap_self, RingHom.id_apply]
