discreteSpecialLinearGroupIntRange

Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

URI: https://scilib.ai/kg/mathlib#Matrix.SpecialLinearGroup.discreteSpecialLinearGroupIntRange

← MathLib Explorer

English

For Γ ⊆ GL(Fin 2) Real with IsArithmetic, Γ.HasDetPlusMinusOne.

Русский

Для Γ ⊆ GL(2,Real) при IsArithmetic, Γ.HasDetPlusMinusOne.

LaTeX

$$∀ {Γ : Subgroup (Matrix.GeneralLinearGroup (Fin 2) Real)} [Γ.IsArithmetic], Γ.HasDetPlusMinusOne$$

Lean4

instance discreteSpecialLinearGroupIntRange : DiscreteTopology (mapGL (n := n) (R := ℤ) ℝ).range :=
  (isEmbedding_mapGL (Isometry.isEmbedding fun _ _ ↦ rfl)).toHomeomorph.discreteTopology

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru