English
If x is a root of p, then the minimal polynomial divides p: minpoly A x ∣ p.
Русский
Если x является корнем p, то минимальный полином делит p.
LaTeX
$$$\\minpoly A x \\mid p \\quad \\text{whenever } aeval x p = 0$$$
Lean4
/-- If an element `x` is a root of a polynomial `p`, then the minimal polynomial of `x` divides `p`.
See also `minpoly.isIntegrallyClosed_dvd` which relaxes the assumptions on `A` in exchange for
stronger assumptions on `B`. -/
theorem dvd {p : A[X]} (hp : Polynomial.aeval x p = 0) : minpoly A x ∣ p :=
by
by_cases hp0 : p = 0
· simp only [hp0, dvd_zero]
have hx : IsIntegral A x := IsAlgebraic.isIntegral ⟨p, hp0, hp⟩
rw [← modByMonic_eq_zero_iff_dvd (monic hx)]
by_contra hnz
apply degree_le_of_ne_zero A x hnz ((aeval_modByMonic_eq_self_of_root (monic hx) (aeval _ _)).trans hp) |>.not_gt
exact degree_modByMonic_lt _ (monic hx)
