Commit 2026-02-05 15:01 b7a750a8

View on Github →

feat: set has cardinality one iff singleton (#28680)

Estimated changes

Modified Mathlib/SetTheory/Cardinal/Basic.lean

deleted theorem Cardinal.mk_emptyCollection_iff

added theorem Cardinal.mk_set_eq_one_iff

added theorem Cardinal.mk_set_eq_zero_iff

modified theorem Cardinal.mk_set_ne_zero_iff