Mathlib v3 is deprecated. Go to Mathlib v4

Def equiv.sigma_sum_distrib

Modification history

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