Gamma_mem — Mathlib

English

An element γ ∈ SL(2, Z) lies in Gamma(N) exactly when its entries satisfy the standard congruence relations modulo N.

Русский

Элемент γ ∈ SL(2, Z) принадлежит Gamma(N) тогда и только тогда, когда его элементы удовлетворяют стандартным конгруентным условиям по модулю N.

LaTeX

$$γ ∈ Gamma(N) ↔ (γ00 ≡ 1 mod N) ∧ (γ01 ≡ 0 mod N) ∧ (γ10 ≡ 0 mod N) ∧ (γ11 ≡ 1 mod N)$$

Lean4

@[simp]
theorem Gamma_mem {N} {γ : SL(2, ℤ)} :
    γ ∈ Gamma N ↔ (γ 0 0 : ZMod N) = 1 ∧ (γ 0 1 : ZMod N) = 0 ∧ (γ 1 0 : ZMod N) = 0 ∧ (γ 1 1 : ZMod N) = 1 :=
  by
  rw [Gamma_mem']
  constructor
  · intro h
    simp [← SL_reduction_mod_hom_val N γ, h]
  · intro h
    ext i j
    rw [SL_reduction_mod_hom_val N γ]
    fin_cases i <;> fin_cases j <;> simp only
    exacts [h.1, h.2.1, h.2.2.1, h.2.2.2]

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