Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-12-09 23:54
a4d7dadf
View on Github →
feat:
¬ Subsingleton α ↔ Nontrivial α
(
#8926
)
Estimated changes
Modified
Mathlib/Logic/Nontrivial/Defs.lean
added
theorem
not_subsingleton_iff_nontrivial