Theorem Cardinal.natCast_le_toENat_iff

Modification history

2026-08-31 13:50
Mathlib/SetTheory/Cardinal/Finite.lean
chore: delete deprecated declarations from February 2026 (#43178) …
Deleted Cardinal.natCast_le_toENat_iffView on Github →
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.natCast_le_toENat_iffView on Github →