mathlib3

438b39a7 - feat(set_theory/cardinal/basic): Distributivity of `cardinal.sum` and + (#13643)

feat(set_theory/cardinal/basic): Distributivity of `cardinal.sum` and + (#13643) `cardinal.sum_add_distrib` shows that `cardinal.sum` distributes over +. Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com>