Theorem Matrix.SpecialLinearGroup.continuous_toGL

Modification history

2026-03-23 09:21

Mathlib/Topology/Algebra/Group/Matrix.lean

refactor(Topology/Instances/Matrix): split file (#36984) …

Modified Matrix.SpecialLinearGroup.continuous_toGL View on Github →

2025-09-22 16:57

Mathlib/Topology/Instances/Matrix.lean

feat(Topology/Constructions): `piMap` is inducing / embedding / etc (#29648) …

Added Matrix.SpecialLinearGroup.continuous_toGL View on Github →