Theorem ENat.card_image_of_injOn

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 ENat.card_image_of_injOn View on Github →