two notions of degree

Stream: general

[Jack J Garzella]

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?

[Jalex Stark]

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