divIntMap

Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs

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

← MathLib Explorer

English

divIntMap(r) is the operation of dividing a finite vector by r, componentwise.

Русский

divIntMap(r) — операция деления вектора на r по компонентам.

LaTeX

$$$\mathrm{divIntMap}(r)\; v \;=\; v / r.$$$

Lean4

/-- An abbreviation of the map which divides a integer vector by an integer. -/
abbrev divIntMap (r : ℤ) {m : ℕ} (v : Fin m → ℤ) : Fin m → ℤ :=
  v / r

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

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

Разделы

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

Аффилиация

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