gammaSet_one_eq — Mathlib

English

For N = 1, all gammaSet(1,r,a) coincide with the gcd condition description: gammaSet(1,r,a) = { v ∈ ℤ^2 : gcd(v_0,v_1)=r }.

Русский

Для N = 1 гамма-наборы совпадают и равны { v ∈ ℤ^2 : gcd(v_0,v_1)=r }.

LaTeX

$$$\gammaSet(1,r,a) = \{ v \in \mathbb{Z}^2 : \gcd(v_0,v_1)=r \}$.$$

Lean4

/-- For level `N = 1`, the gamma sets simplify to only a `gcd` condition. -/
theorem gammaSet_one_eq (a : Fin 2 → ZMod 1) : gammaSet 1 r a = {v : Fin 2 → ℤ | (v 0).gcd (v 1) = r} := by
  simp [gammaSet, Subsingleton.eq_zero]

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