Topic: two notions of degree
Jack J Garzella (Jul 30 2020 at 15:02):
Proving equivalences between
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
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?
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