English
Let c be a cusp for 𝒢. Then for any g ∈ GL(2, ℝ) the image g · c is a cusp for the conjugate action of 𝒢 by g, i.e. for the subgroup ConjAct(g) · 𝒢.
Русский
Пусть c является верховой точкой ( cusp ) для подгруппы 𝒢. Тогда для любого g ∈ GL(2, ℝ) образ g · c является cusp для сопряженного действия: ConjAct(g) · 𝒢.
LaTeX
$$$IsCusp(c, \\mathcal{G}) \\Rightarrow IsCusp(g \\cdot c, \\operatorname{ConjAct}(g) \\cdot \\mathcal{G})$$$
Lean4
theorem smul {c : OnePoint ℝ} {𝒢 : Subgroup (GL (Fin 2) ℝ)} (hc : IsCusp c 𝒢) (g : GL (Fin 2) ℝ) :
IsCusp (g • c) (ConjAct.toConjAct g • 𝒢) :=
by
obtain ⟨p, hp𝒢, hpp, hpc⟩ := hc
refine ⟨_, 𝒢.smul_mem_pointwise_smul _ _ hp𝒢, ?_, ?_⟩
· simpa [ConjAct.toConjAct_smul] using hpp
· simp [ConjAct.toConjAct_smul, MulAction.mul_smul, hpc]
