Commit 2019-12-03 16:50 922a4ebe
View on Github →feat(set_theory/cardinal): eq_one_iff_subsingleton_and_nonempty (#1770)
- feat(set_theory/cardinal): eq_one_iff_subsingleton_and_nonempty From the perfectoid project
- Update src/set_theory/cardinal.lean
feat(set_theory/cardinal): eq_one_iff_subsingleton_and_nonempty (#1770)