Commit 2025-03-11 15:38 756396de
View on Github →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.