English
The map from polynomials to their images in the adjoint algebra is injective when x is integral.
Русский
Отображение полиномов в adjoint алгебру инъективно при условии интегральности x.
LaTeX
$$$\text{Minpoly.ToAdjoin injective}$$$
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.unique` which relaxes the
assumptions on `S` in exchange for stronger assumptions on `R`. -/
theorem _root_.IsIntegrallyClosed.minpoly.unique {s : S} {P : R[X]} (hmo : P.Monic) (hP : Polynomial.aeval s P = 0)
(Pmin : ∀ Q : R[X], Q.Monic → Polynomial.aeval s Q = 0 → degree P ≤ degree Q) : P = minpoly R s :=
by
have hs : IsIntegral R s := ⟨P, hmo, hP⟩
symm; apply eq_of_sub_eq_zero
by_contra hnz
refine IsIntegrallyClosed.degree_le_of_ne_zero hs hnz (by simp [hP]) |>.not_gt ?_
refine degree_sub_lt ?_ (ne_zero hs) ?_
· exact le_antisymm (min R s hmo hP) (Pmin (minpoly R s) (monic hs) (aeval R s))
· rw [(monic hs).leadingCoeff, hmo.leadingCoeff]
