Theorem Cardinal.toENat_le_natCast_iff

Modification history

2024-12-01 00:08
Mathlib/SetTheory/Cardinal/Finite.lean
feat: introduce ENat.card, and use it in place of PartENat.card (#19624)
Added Cardinal.toENat_le_natCast_iffView on Github →