Commit 2025-09-28 10:35 027837c1

chore(RingTheory/Flat): split CharacterModule results from Flat/Basic.lean (#29808) The results requiring character modules require importing a whole set of topological definitions, via AddCircle. This creates a big topological dependency tree for theory that otherwise lives neatly in algebra. As we can see by looking at the 50 or so files losing hundreds of dependencies each! I spotted this as I tried to reduce the amount of analysis and topology imported into the LinearAlgebra folder.