Theorem Cardinal.toENat_congr

Modification history

2024-12-01 00:08

Mathlib/SetTheory/Cardinal/ENat.lean

feat: introduce ENat.card, and use it in place of PartENat.card (#19624)

Added Cardinal.toENat_congr View on Github →