Commit 2024-03-26 18:12 eaede86a

View on Github →

feat(Algebra/Divisibility): generalise mul_dvd_mul_left to Monoid (#11695) mul_dvd_mul_left was implemented for CommMonoid. We have generalised it to Monoid.

Estimated changes

modified theorem mul_dvd_mul_left
modified theorem pow_dvd_pow_of_dvd