finGcdMap_smul

Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs

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

← MathLib Explorer

English

For any integer a and v with finGcdMap(v) = r, one has finGcdMap(a • v) = |a| · r.

Русский

Для любого целого a и вектора v с gcd(v) = r, выполняется finGcdMap(a · v) = |a| · r.

LaTeX

$$$\mathrm{finGcdMap}(a \cdot v) = |a| \cdot r.$$$

Lean4

theorem finGcdMap_smul {r : ℕ} (a : ℤ) {v : Fin 2 → ℤ} (hv : finGcdMap v = r) : finGcdMap (a • v) = a.natAbs * r := by
  simp [finGcdMap, Int.gcd_mul_left, hv]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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