Theorem Matrix.GeneralLinearGroup.continuous_upperRightHom

Modification history

2026-03-23 09:21
Mathlib/Topology/Algebra/Group/Matrix.lean
refactor(Topology/Instances/Matrix): split file (#36984) …
Modified Matrix.GeneralLinearGroup.continuous_upperRightHomView on Github →
2025-10-15 06:00
Mathlib/Topology/Instances/Matrix.lean
feat(GeneralLinearGroup/FinTwo): the addChar sending x to [1,x;0,1] (#30475)
Added Matrix.GeneralLinearGroup.continuous_upperRightHomView on Github →