mathlib

3115ced1 - feat(ring_theory/non_zero_divisors): mul_{left,right}_cancel API (#11211)

feat(ring_theory/non_zero_divisors): mul_{left,right}_cancel API (#11211) Not all `monoid_with_zero` are `cancel_monoid_with_zero`, so we can't use `mul_right_cancel₀` everywhere. However, by definition, multiplication by non-zero-divisors is 0 iff the multiplicand is 0. In the context of a ring, that allows us to `mul_cancel_right` Co-authored-by: Yakov Pechersky <ypechersky@treeline.bio>