Theorem ENat.one_le_card_iff_nonempty

Modification history

2025-10-09 16:24
Mathlib/SetTheory/Cardinal/Finite.lean
feat(Cardinal/Finite): ENat powers and cardinality (#27216) …
Added ENat.one_le_card_iff_nonemptyView on Github →