English
If pb is a power basis and minpoly(K pb.gen) splits in F, then the trace equals the sum of the roots of minpoly_K(pb.gen) in F.
Русский
Если pb — степенной базис, а минимальный многочлен pb.gen над K разлагается в F, то след равно сумме корней минимального многочлена pb.gen в F.
LaTeX
$$$\\operatorname{algebraMap}_{K\\to F}(\\operatorname{trace}_{K,S}(\\mathrm{gen})) = \\sum_{\\alpha \\in (\\minpoly(K,\\mathrm{gen})).\\aroots F} \\alpha$$$
Lean4
/-- Given `pb : PowerBasis K S`, then the trace of `pb.gen` is
`((minpoly K pb.gen).aroots F).sum`. -/
theorem trace_gen_eq_sum_roots [Nontrivial S] (pb : PowerBasis K S) (hf : (minpoly K pb.gen).Splits (algebraMap K F)) :
algebraMap K F (trace K S pb.gen) = ((minpoly K pb.gen).aroots F).sum := by
rw [PowerBasis.trace_gen_eq_nextCoeff_minpoly, RingHom.map_neg, ← nextCoeff_map (algebraMap K F).injective,
nextCoeff_eq_neg_sum_roots_of_monic_of_splits ((minpoly.monic (PowerBasis.isIntegral_gen _)).map _)
((splits_id_iff_splits _).2 hf),
neg_neg]
