finiteIndex_comap — Mathlib

English

IsArithmetic finiteIndex comap relations hold between GL and SL embeddings.

Русский

Сохранение арифметичности и конечного индекса между GL и SL через вложения.

LaTeX

$$IsArithmetic.finiteIndex_comap (𝒢 : Subgroup GL(Fin 2) Real) [IsArithmetic 𝒢] : (𝒢.comap mapGL Real).FiniteIndex$$

Lean4

/-- If `Γ` is arithmetic, its preimage in `SL(2, ℤ)` has finite index. -/
instance finiteIndex_comap (𝒢 : Subgroup (GL (Fin 2) ℝ)) [IsArithmetic 𝒢] : (𝒢.comap (mapGL (R := ℤ) ℝ)).FiniteIndex :=
  ⟨𝒢.index_comap (mapGL (R := ℤ) ℝ) ▸ IsArithmetic.is_commensurable.1⟩

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