Mathlib v3 is deprecated. Go to Mathlib v4

Theorem cardinal.sum_nat_eq_add_sum_succ

Modification history

2022-05-09 14:40
src/set_theory/cardinal/basic.lean
feat(model_theory/language_map): Cardinality of languages with constants (#13981) …
Added cardinal.sum_nat_eq_add_sum_succView on Github →