English
Let 𝒢' ≤ 𝒢 with 𝒢'.relIndex 𝒢 ≠ 0. Then IsCusp c 𝒢' holds if and only if IsCusp c 𝒢 holds.
Русский
Пусть 𝒢' ≤ 𝒢 и relIndex(𝒢', 𝒢) ≠ 0. Тогда IsCusp c 𝒢' эквивалентно IsCusp c 𝒢.
LaTeX
$$$\\mathcal{G}' \\le \\mathcal{G} \\quad \\text{and} \\quad \\mathcal{G}'\\,\\text{relIndex}\\,\\mathcal{G} \\neq 0 \\quad \\Rightarrow\\quad IsCusp(c, \\mathcal{G}') \\iff IsCusp(c, \\mathcal{G})$$$
Lean4
theorem isCusp_iff_of_relIndex_ne_zero {𝒢 𝒢' : Subgroup (GL (Fin 2) ℝ)} (h𝒢 : 𝒢' ≤ 𝒢) (h𝒢' : 𝒢'.relIndex 𝒢 ≠ 0)
(c : OnePoint ℝ) : IsCusp c 𝒢' ↔ IsCusp c 𝒢 :=
by
refine ⟨fun ⟨g, hg, hgp, hgc⟩ ↦ ⟨g, h𝒢 hg, hgp, hgc⟩, fun ⟨g, hg, hgp, hgc⟩ ↦ ?_⟩
obtain ⟨n, hn, -, hgn⟩ := Subgroup.exists_pow_mem_of_relIndex_ne_zero h𝒢' hg
refine ⟨g ^ n, (Subgroup.mem_inf.mpr hgn).1, hgp.pow hn.ne', ?_⟩
rw [Nat.pos_iff_ne_zero] at hn
rwa [(hgp.pow hn).smul_eq_self_iff, hgp.parabolicFixedPoint_pow hn, ← hgp.smul_eq_self_iff]
