Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes