## Stream: new members

### Topic: fundamental theorem of algebra

#### Mii Nguyen (Apr 05 2019 at 10:31):

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 (Apr 05 2019 at 10:43):

(H : degree p ≥ 1)

#### Johan Commelin (Apr 05 2019 at 10:56):

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

#### Mii Nguyen (Apr 05 2019 at 11:02):

@Johan Commelin I didn't update that

#### Johan Commelin (Apr 05 2019 at 11:02):

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

#### Mii Nguyen (Apr 05 2019 at 11:06):

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

Last updated: May 17 2021 at 21:12 UTC