mathlib

ea710ca6 - feat(data/polynomial/ring_division): golf and generalize `leading_coeff_div_by_monic_of_monic` (#11077)

feat(data/polynomial/ring_division): golf and generalize `leading_coeff_div_by_monic_of_monic` (#11077) No longer require that the underlying ring is a domain. Also added helper API lemma `leading_coeff_monic_mul`.