Theorem Cardinal.mk_set_eq_one_iff

Modification history

2026-02-05 15:01
Mathlib/SetTheory/Cardinal/Basic.lean
feat: set has cardinality one iff singleton (#28680)
Added Cardinal.mk_set_eq_one_iffView on Github →