Mathlib Changelog
v4
Changelog
About
Github
Theorem
isDomain_iff_cancelMulZero_and_nontrivial
Modification history
2024-01-05 13:39
Mathlib/Algebra/Ring/Basic.lean
feat(Mathlib/Algebra/Ring/Basic): Subsingleton, NoZeroDivisors and IsDomain (#9407) …
Added
isDomain_iff_cancelMulZero_and_nontrivial
View on Github →