English
If x lies in the base ring K, and S is an algebra over K with finite basis indexed by ι, then the norm of algebraMap_K^S(x) equals x raised to the cardinality of the index set ι.
Русский
Если x принадлежит базовому кольцу K, то норма от образа x в S равна x^{|ι|}, где ι — индексируемый базис S как K-модуля.
LaTeX
$$$ \\operatorname{norm}_R(\\mathrm{algebraMap}_R^S x) = x^{|\\iota|} $$$
Lean4
/-- If `x` is in the base ring `K`, then the norm is `x ^ [L : K]`. -/
theorem norm_algebraMap_of_basis [Fintype ι] (b : Basis ι R S) (x : R) :
norm R (algebraMap R S x) = x ^ Fintype.card ι :=
by
haveI := Classical.decEq ι
rw [norm_apply, ← det_toMatrix b, lmul_algebraMap]
convert @det_diagonal _ _ _ _ _ fun _ : ι => x
· ext (i j); rw [toMatrix_lsmul]
· rw [Finset.prod_const, Finset.card_univ]
