Commit 2022-12-05 14:00 b1d911ac
View on Github →chore(algebra/ring/defs): refactor is_domain (#17721)
Refactor the definiton of is_domain to use is_cancel_mul_zero instead of no_zero_divisors. This is the correct property for a semiring (to do in a future refactor).
Corresponding mathlib4 PR https://github.com/leanprover-community/mathlib4/pull/799.
- depends on #17716