Theorem ENat.card_eq_coe_natCard

Modification history

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