Theorem Matrix.SpecialLinearGroup.isClosedEmbedding_mapGLInt

Modification history

2025-09-22 16:57
Mathlib/NumberTheory/ModularForms/ArithmeticSubgroups.lean
feat(Topology/Constructions): `piMap` is inducing / embedding / etc (#29648) …
Added Matrix.SpecialLinearGroup.isClosedEmbedding_mapGLIntView on Github →