English
Over an algebraically closed field of characteristic zero, a nonzero polynomial f divides f'·g iff the roots of f are contained in the roots of g.
Русский
В алгебраически закрытом поле характеристики ноль, непусть f делит f'·g тогда и только тогда, когда корни f содержатся в корнях g.
LaTeX
$$f ≠ 0 ∧ (∀ x, f(x)=0 ⇒ g(x)=0) ⇔ f | f'·g$$
Lean4
/-- Over an algebraically closed field of characteristic zero a necessary and 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 integral domain, this is a sufficient but not necessary
condition. See `isRoot_of_isRoot_of_dvd_derivative_mul` -/
theorem isRoot_of_isRoot_iff_dvd_derivative_mul {K : Type*} [Field K] [IsAlgClosed K] [CharZero K] {f g : K[X]}
(hf0 : f ≠ 0) : (∀ x, IsRoot f x → IsRoot g x) ↔ f ∣ f.derivative * g :=
by
refine ⟨?_, isRoot_of_isRoot_of_dvd_derivative_mul hf0⟩
by_cases hg0 : g = 0
· simp [hg0]
by_cases hdf0 : derivative f = 0
· rw [eq_C_of_derivative_eq_zero hdf0]
simp only [derivative_C, zero_mul, dvd_zero, implies_true]
have hdg : f.derivative * g ≠ 0 := mul_ne_zero hdf0 hg0
classical rw [Splits.dvd_iff_roots_le_roots (IsAlgClosed.splits f) hf0 hdg, Multiset.le_iff_count]
simp only [count_roots, rootMultiplicity_mul hdg]
refine forall_imp fun a => ?_
by_cases haf : f.eval a = 0
· have h0 : 0 < f.rootMultiplicity a := (rootMultiplicity_pos hf0).2 haf
rw [derivative_rootMultiplicity_of_root haf]
intro h
calc
rootMultiplicity a f = rootMultiplicity a f - 1 + 1 := (Nat.sub_add_cancel (Nat.succ_le_iff.1 h0)).symm
_ ≤ rootMultiplicity a f - 1 + rootMultiplicity a g :=
add_le_add le_rfl (Nat.succ_le_iff.1 ((rootMultiplicity_pos hg0).2 (h haf)))
· simp [haf, rootMultiplicity_eq_zero haf]
