finGcdMap

Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs

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

English

There is a natural bijection gammaSetDivGcdEquiv(r): gammaSet(1,r,0) ≃ gammaSet(1,1,0).

Русский

Существует естественная биекция gammaSetDivGcdEquiv(r): gammaSet(1,r,0) ≃ gammaSet(1,1,0).

LaTeX

$$$\gammaSetDivGcdEquiv(r) : \gammaSet(1,r,0) \simeq \gammaSet(1,1,0).$$$

Lean4

/-- The map from `Fin 2 → ℤ` sending `![a,b]` to `a.gcd b`. -/
abbrev finGcdMap (v : Fin 2 → ℤ) : ℕ :=
  (v 0).gcd (v 1)

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

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

Разделы

Аффилиация

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