conjGL_coe — Mathlib

English

Conjugation by any g in ConjAct SL(2, Z) leaves GammaN invariant: g • GammaN = GammaN.

Русский

Конъгурация любым g из ConjAct SL(2, Z) оставляет Gamma_N неизменной: g • Gamma_N = Gamma_N.

LaTeX

$$$$ g \cdot \Gamma_N = \Gamma_N \quad (\text{for all } g \in \text{ConjAct } SL(2,\mathbb{Z})). $$$$

Lean4

@[simp]
theorem conjGL_coe (Γ : Subgroup SL(2, ℤ)) (g : SL(2, ℤ)) : conjGL Γ g = (toConjAct g⁻¹) • Γ :=
  by
  ext x
  simp_rw [mem_conjGL, ← map_inv, ← map_mul, toGL_injective.eq_iff, map_intCast_injective.eq_iff, exists_eq_right,
    toConjAct_inv, Subgroup.mem_inv_pointwise_smul_iff, toConjAct_smul]

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