English
If x is integral over K, then the trace from L to F of x equals minus the nextCoeff of its minimal polynomial, up to algebraic conjugacy along a tower.
Русский
Если x интегрирован над K, след от x в L к F равен минус следующему коэффициенту минимального многочлена до сопряжения через тождество цепной структуры.
LaTeX
$$$\\operatorname{trace}_{K,L}(x) = -(\\minpoly(K,x)).nextCoeff$$$
Lean4
/-- Trace of the generator of a simple adjoin equals negative of the next coefficient of
its minimal polynomial coefficient. -/
theorem trace_adjoinSimpleGen {x : L} (hx : IsIntegral K x) :
trace K K⟮x⟯ (AdjoinSimple.gen K x) = -(minpoly K x).nextCoeff := by
simpa [minpoly_gen K x] using PowerBasis.trace_gen_eq_nextCoeff_minpoly <| adjoin.powerBasis hx
