Theorems · Theorem · field theory

Polynomial.isRoot_of_isRoot_iff_dvd_derivative_mul

∀ {K : Type u_1} [inst : Field K] [IsAlgClosed K] [CharZero K] {f g : Polynomial K},
  f ≠ 0 → ((∀ (x : K), f.IsRoot x → g.IsRoot x) ↔ f ∣ Polynomial.derivative f * g)

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

Defined in

Mathlib.FieldTheory.IsAlgClosed.Basic

Cited by

0 results in Mathlib

Foundations

Depth 141 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldIsAlgClosedCharZero