Theorem ENat.toNat_card

Modification history

2026-10-28 01:55

Mathlib/SetTheory/Cardinal/Finite.lean

feat(SetTheory/Cardinal/Finite): simp lemmas for `[E]Nat.card` (#44408) …

Added ENat.toNat_card View on Github →