Commit 2024-08-30 01:03 5c9109f1

feat: disjoint union of topological spaces is commutative and associative (#15982) These results are fully analogous to existing results about products, but are missing in mathlib. While at it, also add the four-way commutativity sumSumSumComm, whose product analogue is already in mathlib. Extracted from the bordism theory branch (which wants to prove smooth analogues of these results).