Commit 2024-12-19 20:34 c9f97ab5

chore(Topology/Algebra/Module): split large file (#20036) Split up Mathlib.Topology.Algebra.Module.Basic (> 2500 lines) into several smaller files:

• Mathlib.Topology.Algebra.Module.Basic: topological modules and submodules
• Mathlib.Topology.Algebra.Module.LinearMap: continuous linear maps
• Mathlib.Topology.Algebra.Module.LinearMapPiProd: pi and prod constructions
• Mathlib.Topology.Algebra.Module.Equiv: theory of ContinuousLinearEquivs I found it hard to find natural splitting points, so two of the resulting files (LinearMap and Equiv) are still slightly over 1000 lines.