Zulip Chat Archive

Stream: general

Topic: two notions of degree

view this post on Zulip Jack J Garzella (Jul 30 2020 at 15:02):

Proving equivalences between degree and nat_degree for polynomials has in my (granted, only a few months of) experience been a cause of great pain--mostly because with_bot ℕ doesn't play well with simp and ring. Yet, what at first glance seems to me to be a benefit of using degree, which is knowing that degree f = 0 implies immediately that f ≠ 0, hasn't really come up in proofs about polynomials that I've done.

What if we just removed degree from mathlib? Other than that it would be a huge messy refactor, would there be big drawbacks?

view this post on Zulip Jalex Stark (Jul 30 2020 at 15:19):

I have the same question. I ~always use nat_degree instead of degree.

Last updated: May 14 2021 at 06:16 UTC