English
If x ∈ K and L is a finite-dimensional K-algebra, then the norm from K to L of algebraMap_K^L(x) equals x raised to the dim_K L.
Русский
Если x ∈ K и L — конечномерная K-алгебра, то норма от algebraMap_K^L(x) равна x^{dim_K L}.
LaTeX
$$$ \\operatorname{norm}_K(\\mathrm{algebraMap}_K^L x) = x^{\\operatorname{finrank} K L} $$$
Lean4
/-- If `x` is in the base field `K`, then the norm is `x ^ [L : K]`.
(If `L` is not finite-dimensional over `K`, then `norm = 1 = x ^ 0 = x ^ (finrank L K)`.)
-/
@[simp]
protected theorem norm_algebraMap {L : Type*} [Ring L] [Algebra K L] (x : K) :
norm K (algebraMap K L x) = x ^ finrank K L :=
by
by_cases H : ∃ s : Finset L, Nonempty (Basis s K L)
· rw [norm_algebraMap_of_basis H.choose_spec.some, finrank_eq_card_basis H.choose_spec.some]
· rw [norm_eq_one_of_not_exists_basis K H, finrank_eq_zero_of_not_exists_basis, pow_zero]
assumption_mod_cast
