Commit 2025-09-22 16:57 44b42c1a

feat(Topology/Constructions): piMap is inducing / embedding / etc (#29648) Assorted topological results about Pi types, matrices, and matrix groups:

• An arbitrary product of topologically inducing maps is inducing, and similarly for embeddings, etc.
• As a special case, inducing / embedding / etc maps of topological rings induce maps with the same property on matrix spaces.
• When R is a topological ring and n a fintype, SL n R (with the topology it inherits from Matrix n n R) is a topological group, and its topology coincides with the subspace topology from GL n R.
• The image of SL n Z in GL n R is discrete.