Commit 2025-03-06 22:49 45b1912d

chore(Topology): reverse Homeomorph <-> mulTSupport import (#22645) This moves a lemma from Topology/Homeomorph.lean to Topology/Algebra/Support.lean in order to reverse the import direction. We get a local slight bump as a consequence. It's much smaller than the overall reduction in imports. (I noticed that Topology.Algebra.Group imports Module, so I tried figuring out where it comes from. It seems enough of its dependencies still bring in Module that it's probably not worth pursuing this further, but at least we can eliminate the import in a few other places.)