Theorem not_subsingleton_iff_nontrivial

Modification history

2025-07-29 03:01
Mathlib/Logic/Nontrivial/Defs.lean
chore: some whitespace fixes (#27485) …
Modified not_subsingleton_iff_nontrivialView on Github →
2023-12-09 23:54
Mathlib/Logic/Nontrivial/Defs.lean
feat: `¬ Subsingleton α ↔ Nontrivial α` (#8926)
Added not_subsingleton_iff_nontrivialView on Github →