English
The minimal polynomial is irreducible (reiterated statement).
Русский
Минполином ирредуцируем (повторно).
LaTeX
$$$\\text{Irreducible}(c.minpoly)$$$
Lean4
/-- The minimal polynomial of an element `x` is uniquely characterized by its defining property:
if there is another monic polynomial of minimal degree that has `x` as a root, then this polynomial
is equal to the minimal polynomial of `x`. See also `minpoly.IsIntegrallyClosed.Minpoly.unique`
which relaxes the assumptions on `A` in exchange for stronger assumptions on `B`. -/
theorem unique {p : A[X]} (pmonic : p.Monic) (hp : Polynomial.aeval x p = 0)
(pmin : ∀ q : A[X], q.Monic → Polynomial.aeval x q = 0 → degree p ≤ degree q) : p = minpoly A x :=
by
have hx : IsIntegral A x := ⟨p, pmonic, hp⟩
symm; apply eq_of_sub_eq_zero
by_contra hnz
apply degree_le_of_ne_zero A x hnz (by simp [hp]) |>.not_gt
apply degree_sub_lt _ (minpoly.ne_zero hx)
· rw [(monic hx).leadingCoeff, pmonic.leadingCoeff]
· exact le_antisymm (min A x pmonic hp) (pmin (minpoly A x) (monic hx) (aeval A x))
