English
In the setting of splits, the norm can be written as the product over the roots of the minimal polynomial, pulled back through the algebra map.
Русский
При разложении над основанием норма равна произведению корней минимального полинома, отображенному через алгебраическое отображение.
LaTeX
$$$\\alpha = \\minpoly_K x,\\; \\text{Splits}_{K,F}(\\alpha) \\Rightarrow\\; algebraMap K F(\\mathrm{norm}_K x) = \\prod_{\\beta \\in \\mathrm{aroots}_F(\\alpha)} \\beta$$$
Lean4
theorem norm_eq_prod_roots {x : L} (hF : (minpoly K x).Splits (algebraMap K F)) :
algebraMap K F (norm K x) = ((minpoly K x).aroots F).prod ^ finrank K⟮x⟯ L := by
rw [norm_eq_norm_adjoin K x, map_pow, IntermediateField.AdjoinSimple.norm_gen_eq_prod_roots _ hF]
