conj_cong_is_cong — Mathlib

English

If Γ is a congruence subgrp, then its conjugate by g in GL(2, Z) intersect SL(2, Z) is again a congruence subgroup.

Русский

Если Γ — конгруэнтная подгруппа, то её конъугату по g в GL(2, Z), пересечение с SL(2, Z), снова является конгруэнтной подгруппой.

LaTeX

$$$$ \text{If } \Gamma \text{ is a congruence subgroup, then } (g^{-1} \Gamma g) \cap SL(2,\mathbb{Z}) \text{ is a congruence subgroup for } g \in GL(2,\mathbb{Q}). $$$$

Lean4

theorem conj_cong_is_cong (g : ConjAct SL(2, ℤ)) (Γ : Subgroup SL(2, ℤ)) (h : IsCongruenceSubgroup Γ) :
    IsCongruenceSubgroup (g • Γ) := by
  obtain ⟨N, HN⟩ := h
  refine ⟨N, ?_⟩
  rw [← Gamma_cong_eq_self N g, Subgroup.pointwise_smul_le_pointwise_smul_iff]
  exact HN

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