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