isCusp_iff — Mathlib

English

If two subgroups are commensurable, they share the same cusp property for any cusp.

Русский

Если две подгруппы взаимно односвязны (commensurable), то любая cusp-ассоциированная характеристика одинакова для обеих подгрупп.

LaTeX

$$$\\mathcal{G}, \\mathcal{G}' \\text{ commensurable} \\;\\Rightarrow\\; \\forall c,\\; IsCusp(c, \\mathcal{G}) \\iff IsCusp(c, \\mathcal{G}')$$$

Lean4

theorem isCusp_iff {𝒢 𝒢' : Subgroup (GL (Fin 2) ℝ)} (h𝒢 : Commensurable 𝒢 𝒢') {c : OnePoint ℝ} :
    IsCusp c 𝒢 ↔ IsCusp c 𝒢' :=
  by
  rw [← isCusp_iff_of_relIndex_ne_zero inf_le_left, isCusp_iff_of_relIndex_ne_zero inf_le_right]
  · simpa [Subgroup.inf_relIndex_right] using h𝒢.1
  · simpa [Subgroup.inf_relIndex_left] using h𝒢.2

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