Commit 2025-03-11 15:38 756396de

chore(Topology/Constructions): split out results about sums, products and distributivity (#22827) And move all homeomorphism related to direct sums, products and distributivity into the new file. This resolves a large file warning. It mostly reduces transitive imports (and causes mild increases in other places, and didn't import Homeomorph.Defs before). This is also necessary to break an import cycle in https://github.com/leanprover-community/mathlib4/pull/22137.