English
Let x ∈ L with minpoly K x splits in F; then the trace equals the sum of roots of minpoly_K x in F.
Русский
Пусть x ∈ L, минимальный многочлен K x раскладывается в F; след равна сумме корней minpoly_K x в F.
LaTeX
$$$\\operatorname{algebraMap}_{K\\to F}(\\operatorname{trace}_{K,K\\langle x\\rangle}(\\mathrm{AdjoinSimple.gen\\,K\\,x})) = (\\minpoly(K,x)).\\aroots F.\\text{sum}$$$
Lean4
theorem trace_gen_eq_sum_roots (x : L) (hf : (minpoly K x).Splits (algebraMap K F)) :
algebraMap K F (trace K K⟮x⟯ (AdjoinSimple.gen K x)) = ((minpoly K x).aroots F).sum :=
by
have injKxL := (algebraMap K⟮x⟯ L).injective
by_cases hx : IsIntegral K x; swap
· simp [minpoly.eq_zero hx, trace_gen_eq_zero hx, aroots_def]
rw [← adjoin.powerBasis_gen hx, (adjoin.powerBasis hx).trace_gen_eq_sum_roots] <;>
rw [adjoin.powerBasis_gen hx, ← minpoly.algebraMap_eq injKxL] <;>
try simp only [AdjoinSimple.algebraMap_gen _ _]
exact hf
