Commit 2022-12-06 14:16 52832aea

View on Github →

chore: refactor is_domain (#799) Refactor the definiton of IsDomain to use IsCancelMulZero instead of NoZeroDivisors. This is the correct property for a semiring (to do in a future refactor). We also fix some names in Algebra.Group.Defs. Corresponding mathlib3 PR [#17721](https://github.com/leanprover-community/mathlib/pull/17721).

Estimated changes

Modified Mathlib/Algebra/Group/Defs.lean

added theorem CommSemigroup.IsLeftCancelMul.toIsCancelMul

added theorem CommSemigroup.IsLeftCancelMul.toIsRightCancelMul

deleted theorem CommSemigroup.IsLeftCancelMul.to_IsCancelMul

deleted theorem CommSemigroup.IsLeftCancelMul.to_IsRightCancelMul

added theorem CommSemigroup.IsRightCancelMul.toIsCancelMul

added theorem CommSemigroup.IsRightCancelMul.toIsLeftCancelMul

deleted theorem CommSemigroup.IsRightCancelMul.to_IsCancelMul

deleted theorem CommSemigroup.IsRightCancelMul.to_IsLeftCancelMul

Modified Mathlib/Algebra/Ring/Basic.lean

added theorem IsLeftCancelMulZero.toNoZeroDivisors

added theorem IsRightCancelMulZero.toNoZeroDivisors

added theorem NoZeroDivisors.toIsDomain

Modified Mathlib/Algebra/Ring/Defs.lean

Modified Mathlib/Algebra/Ring/Regular.lean