Commit 2025-12-22 19:35 c96081d9

View on Github →

feat(SetTheory/Cardinal): formulas for sum (fun n : ℕ ↦ x ^ n) (#32645)

Estimated changes

Modified Mathlib/SetTheory/Cardinal/Arithmetic.lean

added theorem Cardinal.mk_list_eq_max

added theorem Cardinal.sum_pow_eq_max_aleph0

added theorem Cardinal.sum_pow_le_max_aleph0

Modified Mathlib/SetTheory/Cardinal/Basic.lean

modified theorem Cardinal.mk_list_eq_sum_pow

added theorem Cardinal.sum_zero_pow

Modified Mathlib/SetTheory/Cardinal/Defs.lean

added theorem Cardinal.nonempty_out