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,