Zulip Chat Archive

Stream: new members

Topic: fundamental theorem of algebra


view this post on Zulip 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?

view this post on Zulip Kenny Lau (Apr 05 2019 at 10:43):

(H : degree p ≥ 1)

view this post on Zulip Johan Commelin (Apr 05 2019 at 10:56):

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

view this post on Zulip Mii Nguyen (Apr 05 2019 at 11:02):

@Johan Commelin I didn't update that

view this post on Zulip 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.

view this post on Zulip 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