Commit 2026-03-23 09:21 a29591aa

refactor(Topology/Instances/Matrix): split file (#36984) The file Topology/Instances/Matrix.lean imports quite a lot of algebra files, which are only used at the very end of the file, when considering the topology of the matrix groups GL(n) and SL(n). This PR splits off the material on matrix groups to a separate file, which results in a very substantial decrease in the number of imports downstream (~100 fewer imports in ~300 files).