Commit 2021-08-09 15:47 3dd83166
View on Github →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.
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.