English
An explicit formula for the norm map: algebraMap K L (Algebra.norm K x) = ∏ i ∈ Finset.range(rank_K L) x^{(|K|)^i}.
Русский
Явная формула нормы: algebraMap(K,L)(norm_K L(x)) = ⋯ произведение по i до rank_K L of x^{|K|^i}.
LaTeX
$$$$ \\mathrm{algebraMap}(K,L)(\\\\mathrm{norm}(K,x)) = \\prod_{i=0}^{\\\\mathrm{finrank}_K L - 1} x^{(|K|)^{i}}. $$$$
Lean4
/-- An explicit formula for the norm map: `norm[L/K](x) = ∏ i < [L:K], x ^ ((#K) ^ i)`. -/
theorem algebraMap_norm_eq_prod_pow :
algebraMap K L (Algebra.norm K x) = ∏ i ∈ Finset.range (Module.finrank K L), x ^ (Nat.card K ^ i) :=
by
have := Finite.of_injective _ (FaithfulSMul.algebraMap_injective K L)
have := ofFinite K
rw [Algebra.norm_eq_prod_automorphisms, Finset.prod_range]
exact
Eq.symm <|
prod_bijective _ (bijective_frobeniusAlgEquivOfAlgebraic_pow K L) _ _ <| fun i ↦ by
rw [AlgEquiv.coe_pow, coe_frobeniusAlgEquivOfAlgebraic_iterate, card_eq_nat_card]
