Theorem isCancelMulZero_iff_noZeroDivisors

Modification history

2025-08-11 11:23
Mathlib/Algebra/Ring/Basic.lean
feat(Algebra): connect IsRegular/IsCancelMul to nonZeroDivisors/NoZeroDivisors (#27877) …
Modified isCancelMulZero_iff_noZeroDivisorsView on Github →
2024-06-14 14:02
Mathlib/Algebra/Ring/Basic.lean
chore: generalize some results to non-unital rings (#13807)
Modified isCancelMulZero_iff_noZeroDivisorsView on Github →
2024-01-05 13:39
Mathlib/Algebra/Ring/Basic.lean
feat(Mathlib/Algebra/Ring/Basic): Subsingleton, NoZeroDivisors and IsDomain (#9407) …
Added isCancelMulZero_iff_noZeroDivisorsView on Github →