Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-28 05:04 1e72d86f

View on Github →

chore(data/polynomial/degree/lemmas + data/polynomial/ring_division): move lemmas, reduce assumptions, golf (#12858) This PR takes advantage of the reduced assumptions that are a consequence of #12854. Again, I moved two lemmas from their current location to a different file, where the typeclass assumptions make more sense,

Estimated changes