proj_dioph

Mathlib.NumberTheory.Dioph

URI: https://scilib.ai/kg/mathlib#Dioph.proj_dioph

English

The i-th coordinate projection is Diophantine: the map v ↦ v(i) is Diophantine.

Русский

i-й координатный проекционный функционал диагофантов; проекция i-го координаты диагофантова.

LaTeX

$$$$\mathrm{DiophFn}(\lambda v: v(i))$$$$

Lean4

theorem proj_dioph (i : α) : DiophFn fun v => v i :=
  abs_poly_dioph (Poly.proj i)

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

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

Разделы

Аффилиация

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