Commit 2022-04-25 23:11 438b39a7

View on Github →

feat(set_theory/cardinal/basic): Distributivity of cardinal.sum and + (#13643) cardinal.sum_add_distrib shows that cardinal.sum distributes over +.

Estimated changes

Modified src/logic/equiv/basic.lean

added def equiv.sigma_sum_distrib

Modified src/set_theory/cardinal/basic.lean

added theorem cardinal.sum_add_distrib