algebraMap_norm_eq_pow_sum — Mathlib

English

An explicit formula for the norm map: algebraMap K L (Algebra.norm K x) = x^{ sum_{i < rank_K L} |K|^i }.

Русский

Явная формула нормы через сумму степеней: algebraMap(K,L)(norm_K L(x)) = x^{∑_{i<rank_K L} |K|^i}.

LaTeX

$$$$ \\mathrm{algebraMap}(K,L)(\\\\mathrm{norm}(K,x)) = x^{\\\\sum_{i=0}^{\\\\mathrm{finrank}_K L - 1} |K|^{i}}. $$$$

Lean4

/-- An explicit formula for the norm map: `norm[L/K](x) = x ^ (∑ i < [L:K], (#K) ^ i)`. -/
theorem algebraMap_norm_eq_pow_sum :
    algebraMap K L (Algebra.norm K x) = x ^ ∑ i ∈ Finset.range (Module.finrank K L), Nat.card K ^ i := by
  rw [algebraMap_norm_eq_prod_pow, Finset.prod_pow_eq_pow_sum]

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