Little_Bezout_Theorem
Provedalgebrabezoutpolynomial-theoryproofwiki
A polynomial P(x) has root a if and only if (x - a) divides P(x). Equivalently, the remainder when dividing P by (x-a) is P(a).
Preamble
import Mathlib.RingTheory.Polynomial.Basic
Formal statement
theorem Little_Bezout_Theorem {R : Type _} [CommRing R] (p : Polynomial R) (a : R) : Polynomial.IsRoot p a ↔ (Polynomial.X - Polynomial.C a) ∣ p := by sorrySource