instIsArithmeticMapSpecialLinearGroupFinOfNatNatIntGeneralLinearGroupRealMapGLOfFiniteIndex

English

If Γ is arithmetic, its preimage in SL(2,ℤ) has finite index.

Русский

Если Γ арифметическая, её предобраз в SL(2,ℤ) имеет конечный индекс.

LaTeX

$$finiteIndex_comap (𝒢) [IsArithmetic 𝒢] : (𝒢.comap mapGL).FiniteIndex$$

Lean4

/-- Images in `GL(2, ℝ)` of finite-index subgroups of `SL(2, ℤ)` are arithmetic. -/
instance (Γ : Subgroup SL(2, ℤ)) [Γ.FiniteIndex] : IsArithmetic Γ :=
  isArithmetic_iff_finiteIndex.mpr ‹_›

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