Commit 2026-04-15 08:53 7eb14934
View on Github →feat(Topology/Algebra/Group/Matrix): refactor; continuity of maps on GL(n) and SL(n) (#37601)
Show that the maps Rˣ → Sˣ, SL n R → SL n S, and GL n R → GL n S induced by a ring/monoid morphism f : R → S are continuous / inducing / embedding / closed-embedding if f is.
Also add Real analogues of some existing Complex lemmas about the intCast map, e.g. Real.closedEmbedding_intCast, and refactor and clean up Topology/Algebra/Group/Matrix.lean.