Commit 2021-12-31 21:03 ea710ca6
View on Github →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.