Stream: new members
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