English
The unique' theorem asserts that if p is monic, p(x) = 0 and a certain minimality condition holds for all q with lower degree, then p = minpoly_A(x).
Русский
Единственность: если p моноический, p(x)=0 и для всех q степени меньше p выполняется минимальное условие, тогда p = minpoly_A(x).
LaTeX
$$$p\\text{ моноик},\\ p(x)=0,\\ (\\forall q: A[X],\\ deg q < deg p \\Rightarrow (q=0 \\lor aeval_x q \\neq 0)) \\Rightarrow p = \\minpoly_{A}(x).$$$
Lean4
theorem unique' {p : A[X]} (hm : p.Monic) (hp : Polynomial.aeval x p = 0)
(hl : ∀ q : A[X], degree q < degree p → q = 0 ∨ Polynomial.aeval x q ≠ 0) : p = minpoly A x :=
by
nontriviality A
have hx : IsIntegral A x := ⟨p, hm, hp⟩
obtain h | h := hl _ ((minpoly A x).degree_modByMonic_lt hm)
swap
· exact (h <| (aeval_modByMonic_eq_self_of_root hm hp).trans <| aeval A x).elim
obtain ⟨r, hr⟩ := (modByMonic_eq_zero_iff_dvd hm).1 h
rw [hr]
have hlead := congr_arg leadingCoeff hr
rw [mul_comm, leadingCoeff_mul_monic hm, (monic hx).leadingCoeff] at hlead
have : natDegree r ≤ 0 :=
by
have hr0 : r ≠ 0 := by
rintro rfl
exact ne_zero hx (mul_zero p ▸ hr)
apply_fun natDegree at hr
rw [hm.natDegree_mul' hr0] at hr
apply Nat.le_of_add_le_add_left
rw [add_zero]
exact hr.symm.trans_le (natDegree_le_natDegree <| min A x hm hp)
rw [eq_C_of_natDegree_le_zero this, ← Nat.eq_zero_of_le_zero this, ← leadingCoeff, ← hlead, C_1, mul_one]
