Commit 2024-01-05 13:39 e3d1c7ac

View on Github →

feat(Mathlib/Algebra/Ring/Basic): Subsingleton, NoZeroDivisors and IsDomain (#9407) Added some results relating NoZeroDivisors and IsDomain for Ring.

Estimated changes

Modified Mathlib/Algebra/Ring/Basic.lean

added theorem isCancelMulZero_iff_isDomain_or_subsingleton

added theorem isCancelMulZero_iff_noZeroDivisors

added theorem isDomain_iff_cancelMulZero_and_nontrivial

added theorem isDomain_iff_noZeroDivisors_and_nontrivial

added theorem noZeroDivisors_iff_isDomain_or_subsingleton