Theorem ENat.card_eq_one_iff_unique

Modification history

2025-10-09 16:24

Mathlib/SetTheory/Cardinal/Finite.lean

feat(Cardinal/Finite): ENat powers and cardinality (#27216) …

Added ENat.card_eq_one_iff_unique View on Github →