feat(Topology/Algebra/Group/Matrix): refactor; continuity of maps on GL(n) and SL(n)

[loefflerd]

Show that the map GL n R → GL n S induced by a ring morphism f : R → S is continuous if f is (and similarly if f is inducing, embedding, or closed embedding). Also refactor and clean up Topology/Algebra/Group/Matrix.lean.

---

[github-actions]

PR summary fb17c7c573

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ Topology.IsClosedEmbedding.prodMap
+ _root_.Continuous.generalLinearGroup_map
+ _root_.Continuous.specialLinearGroup_map
+ _root_.Topology.IsClosedEmbedding.generalLinearGroup_map
+ _root_.Topology.IsClosedEmbedding.specialLinearGroup_map
+ _root_.Topology.IsClosedEmbedding.units_map
+ _root_.Topology.IsEmbedding.generalLinearGroup_map
+ _root_.Topology.IsEmbedding.specialLinearGroup_map
+ _root_.Topology.IsEmbedding.units_map
+ _root_.Topology.IsInducing.generalLinearGroup_map
+ _root_.Topology.IsInducing.specialLinearGroup_map
+ _root_.Topology.IsInducing.units_map
+ closedEmbedding_intCast
+ continuous_mapGL
+ instT1Space
+ isClosedEmbedding_mapGL
+ isClosed_range_intCast
+ isOpen_compl_range_intCast
+ isometry_intCast

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

Decrease in tech debt: (relative, absolute) = (2.00, 0.00)

Current number	Change	Type
6899	-2	backward.isDefEq.respectTransparency

Current commit 31ba9b9eff
Reference commit fb17c7c573

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).