Mathlib v3 is deprecated. Go to Mathlib v4

Theorem cardinal.sum_add_distrib

Modification history

2022-04-25 23:11
src/set_theory/cardinal/basic.lean
feat(set_theory/cardinal/basic): Distributivity of `cardinal.sum` and + (#13643) …
Added cardinal.sum_add_distribView on Github →