mathlib3

1e72d86f - chore(data/polynomial/degree/lemmas + data/polynomial/ring_division): move lemmas, reduce assumptions, golf (#12858)

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,