smul_of_mem — Mathlib

English

If g belongs to 𝒢, then g · c is still a cusp for 𝒢 (the same subgroup).

Русский

Если g ∈ 𝒢, то c cusp-образа g·c остаётся cusp для той же подгруппы 𝒢.

LaTeX

$$$g \\in \\mathcal{G} \\Rightarrow IsCusp(g \\cdot c, \\mathcal{G})$$$

Lean4

theorem smul_of_mem {c : OnePoint ℝ} {𝒢 : Subgroup (GL (Fin 2) ℝ)} (hc : IsCusp c 𝒢) {g : GL (Fin 2) ℝ} (hg : g ∈ 𝒢) :
    IsCusp (g • c) 𝒢 := by
  convert hc.smul g
  ext x
  rw [Subgroup.mem_pointwise_smul_iff_inv_smul_mem, ← ConjAct.toConjAct_inv, ConjAct.toConjAct_smul, inv_inv,
    Subgroup.mul_mem_cancel_right _ hg, Subgroup.mul_mem_cancel_left _ (inv_mem hg)]

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