Theorem Matrix.SpecialLinearGroup.isInducing_mapGL

Modification history

2026-04-15 08:53
Mathlib/Topology/Algebra/Group/Matrix.lean
feat(Topology/Algebra/Group/Matrix): refactor; continuity of maps on GL(n) and SL(n) (#37601) …
Modified Matrix.SpecialLinearGroup.isInducing_mapGLView on Github →
2026-03-23 09:21
Mathlib/Topology/Algebra/Group/Matrix.lean
refactor(Topology/Instances/Matrix): split file (#36984) …
Modified Matrix.SpecialLinearGroup.isInducing_mapGLView on Github →
2025-09-22 16:57
Mathlib/Topology/Instances/Matrix.lean
feat(Topology/Constructions): `piMap` is inducing / embedding / etc (#29648) …
Added Matrix.SpecialLinearGroup.isInducing_mapGLView on Github →