isArithmetic_iff_finiteIndex — Mathlib

English

For Γ ⊆ SL(2,ℤ), IsArithmetic Γ ↔ FiniteIndex Γ.

Русский

Для Γ ⊆ SL(2,ℤ) справедливо IsArithmetic Γ ↔ FiniteIndex Γ.

LaTeX

$$IsArithmetic Γ ↔ FiniteIndex Γ$$

Lean4

theorem isArithmetic_iff_finiteIndex {Γ : Subgroup SL(2, ℤ)} : IsArithmetic Γ ↔ Γ.FiniteIndex := by
  constructor <;>
    · refine fun ⟨h⟩ ↦ ⟨?_⟩
      simpa [Commensurable, MonoidHom.range_eq_map, ← relIndex_comap,
        comap_map_eq_self_of_injective mapGL_injective] using h

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