English
Let f,g ∈ R[X] with f ≠ 0 and f ∣ f′ g. Then for any a ∈ R, if f(a)=0, then g(a)=0. Equivalently, every root of f is a root of g.
Русский
Пусть f,g ∈ R[X], f ≠ 0 и f делит f′ g. Тогда для любого a ∈ R, если f(a)=0, то g(a)=0. Иными словами, каждый корень f является корнем g.
LaTeX
$$$f \neq 0 \wedge f \mid f' g \implies \forall a,\ f(a)=0 \Rightarrow g(a)=0.$$$
Lean4
/-- A sufficient condition for the set of roots of a nonzero polynomial `f` to be a subset of the
set of roots of `g` is that `f` divides `f.derivative * g`. Over an algebraically closed field of
characteristic zero, this is also a necessary condition.
See `isRoot_of_isRoot_iff_dvd_derivative_mul` -/
theorem isRoot_of_isRoot_of_dvd_derivative_mul [CharZero R] {f g : R[X]} (hf0 : f ≠ 0) (hfd : f ∣ f.derivative * g)
{a : R} (haf : f.IsRoot a) : g.IsRoot a := by
rcases hfd with ⟨r, hr⟩
have hdf0 : derivative f ≠ 0 := by
contrapose! haf
rw [eq_C_of_derivative_eq_zero haf] at hf0 ⊢
exact not_isRoot_C _ _ <| C_ne_zero.mp hf0
by_contra hg
have hdfg0 : f.derivative * g ≠ 0 := mul_ne_zero hdf0 (by rintro rfl; simp at hg)
have hr' := congr_arg (rootMultiplicity a) hr
rw [rootMultiplicity_mul hdfg0, derivative_rootMultiplicity_of_root haf, rootMultiplicity_eq_zero hg, add_zero,
rootMultiplicity_mul (hr ▸ hdfg0), add_comm,
Nat.sub_eq_iff_eq_add (Nat.succ_le_iff.2 ((rootMultiplicity_pos hf0).2 haf))] at hr'
cutsat
