gammaSet_one_mem_iff

Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs

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

English

For v ∈ gammaSet(1,r,0), we have gcd(v_0,v_1) = r.

Русский

Пусть 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 gammaSet_one_mem_iff (v : Fin 2 → ℤ) : v ∈ gammaSet 1 r 0 ↔ (v 0).gcd (v 1) = r := by
  simp [gammaSet, Subsingleton.eq_zero]

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

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

Разделы

Аффилиация

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