mathlib3

fd2c6c47 - chore(data/polynomial/ring_division): remove nontrivial assumptions (#12984)

chore(data/polynomial/ring_division): remove nontrivial assumptions (#12984) Additionally, this removes: * some `polynomial.monic` assumptions that can be handled by casing instead * the explicit `R` argument from `is_field.to_field R hR`