surjective_cosetToCuspOrbit — Mathlib

English

The map cosetToCuspOrbit is surjective for arithmetic 𝒢.

Русский

Отображение cosetToCuspOrbit сюръективно для арифметической 𝒢.

LaTeX

$$$(\\cosetToCuspOrbit(\\mathcal{G})).Surjective$$

Lean4

theorem surjective_cosetToCuspOrbit (𝒢 : Subgroup (GL (Fin 2) ℝ)) [𝒢.IsArithmetic] : (cosetToCuspOrbit 𝒢).Surjective :=
  by
  rintro ⟨c, (hc : IsCusp c _)⟩
  rw [Subgroup.IsArithmetic.isCusp_iff_isCusp_SL2Z, isCusp_SL2Z_iff'] at hc
  obtain ⟨g, rfl⟩ := hc
  use ⟦g⁻¹⟧
  aesop

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