English
Let f ∈ K[X] be nonzero and let pb be a power basis for the K-algebra generated by a root of f. Then the minimal polynomial of the generator of pb is f multiplied by the inverse of its leading coefficient, i.e. minpoly_K((pb).gen) = f · C(f.leadingCoeff)^{-1}.
Русский
Пусть f ∈ K[X] не нуль и пусть pb — базис мощности для расширения над K, генерируемого корнем f. Тогда минимальный многочлен генератора pb равен f, умноженному на обратную ведущей коэффициентa: minpoly_K((pb).gen) = f · C(f.leadingCoeff)^{-1}.
LaTeX
$$$\minpoly_K\bigl((\text{powerBasis}\;hf).gen\bigr) = f \cdot C\bigl(f.leadingCoeff\bigr)^{-1}$$$
Lean4
theorem minpoly_powerBasis_gen (hf : f ≠ 0) : minpoly K (powerBasis hf).gen = f * C f.leadingCoeff⁻¹ := by
rw [powerBasis_gen, minpoly_root hf]
