The fundamental theorem of algebra

TODO

• compare analysis.complex.polynomial
• statment
  • proof
    • (A)
    • (B)
    • (C)
  • Lemma
    • proof

def Polynomial.constant (f : Polynomial ℂ) : Prop

A polynomial is non-constant if its degree is greater than 0.

Equations

• f.constant = (0 < f.degree)

theorem fundamental_theorem_of_algebra (f : Polynomial ℂ) (h : ¬f.constant) : ∃ (z : ℂ), f.IsRoot z