Theorem Set.toENat_cardinalMk

Modification history

2026-10-28 01:55

Mathlib/Data/Set/Card.lean

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

Modified Set.toENat_cardinalMk View on Github →

2025-02-24 09:31

Mathlib/Data/Set/Card.lean

feat(Data/Set/Card): a few missing lemmas (#22186) …

Added Set.toENat_cardinalMk View on Github →