Theorem isDomain_iff_noZeroDivisors_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_noZeroDivisors_and_nontrivial View on Github →