English
If a monic polynomial a strictly divides the minimal polynomial minpoly A x, then a(x) ≠ 0.
Русский
Если монический полином a строго делит минимальный полином minpoly A x, то a(x) ≠ 0.
LaTeX
$$$\operatorname{aeval}_x(a) \neq 0$$$
Lean4
/-- If `a` strictly divides the minimal polynomial of `x`, then `x` cannot be a root for `a`. -/
theorem aeval_ne_zero_of_dvdNotUnit_minpoly {a : A[X]} (hx : IsIntegral A x) (hamonic : a.Monic)
(hdvd : DvdNotUnit a (minpoly A x)) : Polynomial.aeval x a ≠ 0 :=
by
refine fun ha => (min A x hamonic ha).not_gt (degree_lt_degree ?_)
obtain ⟨_, c, hu, he⟩ := hdvd
have hcm := hamonic.of_mul_monic_left (he.subst <| monic hx)
rw [he, hamonic.natDegree_mul hcm]
-- TODO: port Nat.lt_add_of_zero_lt_left from lean3 core
apply lt_add_of_pos_right
refine (lt_of_not_ge fun h => hu ?_)
rw [eq_C_of_natDegree_le_zero h, ← Nat.eq_zero_of_le_zero h, ← leadingCoeff, hcm.leadingCoeff, C_1]
exact isUnit_one
