mathlib3

c7e910fb - chore(data/polynomial/ring_division): remove nontrivial assumptions