Theorem Continuous.generalLinearGroup_map

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) …

Added Continuous.generalLinearGroup_map View on Github →