fundamental theorem of algebra

Stream: new members

[Mii Nguyen]

I try to formal the Fundamental theorem of algebra. Here it's my work:

theorem fundamental_theorem_of_algebra: ∀(p: polynomial ℂ) (degree p ≥ 1), ∃ (z: ℂ), is_root p z := sorry

I would like to declare non-constant polynomial p by using degree p >= 1. But lean demand the condition

⊢ has_le (polynomial ℂ)

that I don't understand. Could somebody help me explain it?

However, I try another formal

theorem fundamental_theorem_of_algebra_2: ∀(p: polynomial ℂ), ∀ (c:ℂ) ( p ≠ C c), ∃ (z: ℂ), is_root p z := sorry

and it work, but I wonder if there are a better method to formal a non-constant polynomial?

[Kenny Lau]

(H : degree p ≥ 1)

[Johan Commelin]

@Mii Nguyen Are you aware of https://github.com/leanprover-community/mathlib/pull/851?

[Mii Nguyen]

@Johan Commelin I didn't update that

[Johan Commelin]

No, it's just that I wondered if you realised that someone else had formalised FTA as well.

[Mii Nguyen]

@Johan Commelin No, I didn't realised it. I study this version of FTA now for understand. Thanks for your info.