English
For a power basis pb, the trace of the generator equals minus the next coefficient of its minimal polynomial.
Русский
Для степенного базиса pb след генератора равен минус следующему коэффициенту минимального многочлена этого элемента.
LaTeX
$$$\\operatorname{trace}_{K,S}(\\mathrm{gen}) = - (\\minpoly(K,\\mathrm{gen})).\\text{nextCoeff}$$$
Lean4
/-- Given `pb : PowerBasis K S`, the trace of `pb.gen` is `-(minpoly K pb.gen).nextCoeff`. -/
theorem trace_gen_eq_nextCoeff_minpoly [Nontrivial S] (pb : PowerBasis K S) :
Algebra.trace K S pb.gen = -(minpoly K pb.gen).nextCoeff :=
by
have d_pos : 0 < pb.dim := PowerBasis.dim_pos pb
have d_pos' : 0 < (minpoly K pb.gen).natDegree := by simpa
haveI : Nonempty (Fin pb.dim) := ⟨⟨0, d_pos⟩⟩
rw [trace_eq_matrix_trace pb.basis, trace_eq_neg_charpoly_coeff, charpoly_leftMulMatrix, ← pb.natDegree_minpoly,
Fintype.card_fin, ← nextCoeff_of_natDegree_pos d_pos']
