mathlib3

3dd83166 - feat(algebra/ring/basic): mul_{left,right}_cancel_of_non_zero_divisor (#8425)

feat(algebra/ring/basic): mul_{left,right}_cancel_of_non_zero_divisor (#8425) We also golf the proof that a domain is a cancel_monoid_with_zero. Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>