Theorem noZeroDivisors_iff_isDomain_or_subsingleton

Modification history

2024-01-05 13:39

Mathlib/Algebra/Ring/Basic.lean

feat(Mathlib/Algebra/Ring/Basic): Subsingleton, NoZeroDivisors and IsDomain (#9407) …

Added noZeroDivisors_iff_isDomain_or_subsingleton View on Github →