mathlib3

922a4ebe - feat(set_theory/cardinal): eq_one_iff_subsingleton_and_nonempty (#1770)

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