Documentation

FormalBook.Chapter_21

The fundamental theorem of algebra #

TODO #

Equations
  • f.constant = (0 < f.degree)
theorem fundamental_theorem_of_algebra (f : Polynomial ) (h : ¬f.constant) :
∃ (z : ), f.IsRoot z