Commit 2025-10-09 16:24 724a6cb9

View on Github →

feat(Cardinal/Finite): ENat powers and cardinality (#27216) This PR continues the work from #25574. Original PR: https://github.com/leanprover-community/mathlib4/pull/25574

Estimated changes

added theorem ENat.epow_add
added theorem ENat.epow_eq_one_iff
added theorem ENat.epow_eq_zero_iff
added theorem ENat.epow_left_mono
added theorem ENat.epow_mul
added theorem ENat.epow_natCast
added theorem ENat.epow_one
added theorem ENat.epow_right_mono
added theorem ENat.epow_top
added theorem ENat.epow_zero
added theorem ENat.mul_epow
added theorem ENat.one_epow
added theorem ENat.one_le_epow
added theorem ENat.top_epow
added theorem ENat.top_epow_top
added theorem ENat.zero_epow
added theorem ENat.zero_epow_top
added theorem ENat.card_fun
modified theorem ENat.card_prod