English
Let K, F be fields and L an algebra over K. For any x ∈ L, if the minimal polynomial of x over K splits in F, then the image in F of the K-norm of AdjoinSimple.gen_K(x) equals the product in F of all roots of that minimal polynomial; i.e., the norm equals the product of its conjugates in F.
Русский
Пусть K, F — поля, L — расщепление над K, и возьмём x ∈ L. Пусть минимальный многочлен minpoly_K(x) распадается в F. Тогда образ norm_K(AdjoinSimple.gen_K x) в F равен произведению всех корней minpoly_K(x) в F.
LaTeX
$$$ (\\operatorname{algebraMap} \\, K\\, F)(\\operatorname{norm} \\, K \\, (\\operatorname{AdjoinSimple.gen} \\, K \\, x)) = ((\\minpoly \\, K \\, x).\\aroots F).\\prod $$$
Lean4
theorem _root_.IntermediateField.AdjoinSimple.norm_gen_eq_prod_roots (x : L)
(hf : (minpoly K x).Splits (algebraMap K F)) :
(algebraMap K F) (norm K (AdjoinSimple.gen K x)) = ((minpoly K x).aroots F).prod :=
by
have injKxL := (algebraMap K⟮x⟯ L).injective
by_cases hx : IsIntegral K x; swap
· simp [minpoly.eq_zero hx, IntermediateField.AdjoinSimple.norm_gen_eq_one hx, aroots_def]
rw [← adjoin.powerBasis_gen hx, PowerBasis.norm_gen_eq_prod_roots] <;>
rw [adjoin.powerBasis_gen hx, ← minpoly.algebraMap_eq injKxL] <;>
simp only [AdjoinSimple.algebraMap_gen _ _, hf]
