Commit 2026-08-24 07:44 437b5822

refactor(Topology/Algebra/Group): split long file Basic.lean (#43010) Split into 7 files:

• Topology.Algebra.Group.Basic (438 lines): translations, conjugation, compactness
• Topology.Algebra.Group.ContinuousDiv (150 lines): continuous division and subtraction
• Topology.Algebra.Group.ContinuousInv (268 lines): continuous inversion and negation
• Topology.Algebra.Group.Neighborhood (310 lines): neighborhood filters, bases, open maps
• Topology.Algebra.Group.Order(131 lines): ordered topological groups
• Topology.Algebra.Group.Subgroup (193 lines): closures and topology of subgroups
• Topology.Algebra.Group.ZPow (70 lines): continuity of integer powers Some material on unit groups (153 lines) was moved to the existing file Topology.Algebra.Group.Units. This split achieves significant import reductions for many downstream files.