Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes