@MISC{UPROOTS.MIZ,
  AUTHOR = {Rudnicki, Piotr},
  TITLE = {Little {B}ezout Theorem (Factor Theorem)},
  NOTE = {This work has been supported by NSERC Grant OGP9207.},
  SECTION1 = {Preliminaries},
  SECTION2 = {Canonical Ordering of a Finite Set},
  SECTION3 = {More about Bags},
  SECTION4 = {More on Polynomials},
  SECTION5 = {Little Bezout Theorem},
  SECTION6 = {Polynomials Defined by Roots},
  DAY = {30},
  MONTH = {December},
  YEAR = {2003},
  ADDRESS1 = {University of Alberta\\Edmonton},
  SUMMARY = {We present a formalization of the factor theorem for univariate
  polynomials, also called the (little) Bezout theorem: Let $r$ belong to a
  commutative ring $L$ and $p(x)$ be a polynomial over $L$. Then $x-r$
  divides $p(x)$ iff $p(r) = 0$.  We also prove some consequences of
  this theorem like that any non zero polynomial of degree $n$ over an
  algebraically closed integral domain has $n$ (non necessarily distinct)
  roots.}}

