Theorem ENat.one_le_epow

Modification history

2026-04-29 14:11
Mathlib/Data/ENat/Pow.lean
chore: make argument in `zero_le`/`one_le` implicit (#38148) …
Modified ENat.one_le_epowView on Github →
2025-10-09 16:24
Mathlib/Data/ENat/Pow.lean
feat(Cardinal/Finite): ENat powers and cardinality (#27216) …
Added ENat.one_le_epowView on Github →