English
Let p be a polynomial and a ∈ R. If m = rootMultiplicity a p, then eval a of p /ₘ (X - C a)^m is nonzero when p ≠ 0.
Русский
Пусть p — полином и a ∈ R. Если m = rootMultiplicity a p, то eval a (p /ₘ (X - C a)^m) ≠ 0 при p ≠ 0.
LaTeX
$$$ \operatorname{eval}_a\left(p /_{\mathrm{monic}} (X - C a)^{\operatorname{rootMultiplicity}(a,p)}\right) \neq 0 \quad \text{if } p \neq 0. $$$
Lean4
theorem eval_divByMonic_pow_rootMultiplicity_ne_zero {p : R[X]} (a : R) (hp : p ≠ 0) :
eval a (p /ₘ (X - C a) ^ rootMultiplicity a p) ≠ 0 := by
classical
haveI : Nontrivial R := Nontrivial.of_polynomial_ne hp
rw [Ne, ← IsRoot, ← dvd_iff_isRoot]
rintro ⟨q, hq⟩
have := pow_mul_divByMonic_rootMultiplicity_eq p a
rw [hq, ← mul_assoc, ← pow_succ, rootMultiplicity_eq_multiplicity, if_neg hp] at this
exact
(finiteMultiplicity_of_degree_pos_of_monic (show (0 : WithBot ℕ) < degree (X - C a) by rw [degree_X_sub_C]; decide)
(monic_X_sub_C _) hp).not_pow_dvd_of_multiplicity_lt
(Nat.lt_succ_self _) (dvd_of_mul_right_eq _ this)
