mem_gammaSet_one

Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs

URI: https://scilib.ai/kg/mathlib#EisensteinSeries.mem_gammaSet_one

English

For N = 1, r arbitrary, v ∈ gammaSet(1,r,0) if and only if gcd(v_0,v_1) = r.

Русский

Для N=1, v ∈ gammaSet(1,r,0) тогда и только тогда, когда gcd(v_0,v_1)=r.

LaTeX

$$$v \in \gammaSet(1,r,0) \iff \gcd(v_0,v_1)=r.$$$

Lean4

theorem mem_gammaSet_one (v : Fin 2 → ℤ) : v ∈ gammaSet 1 1 0 ↔ IsCoprime (v 0) (v 1) := by
  rw [gammaSet_one_mem_iff, Int.isCoprime_iff_gcd_eq_one]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru