const_dioph

Mathlib.NumberTheory.Dioph

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

English

A constant Diophantine function exists for any fixed type with natural codomain.

Русский

Существует диагофантова константа функции для любых фиксированных типов.

LaTeX

$$$$\mathrm{const\,Dioph}(n)$$$$

Lean4

theorem const_dioph (n : ℕ) : DiophFn (const (α → ℕ) n) :=
  abs_poly_dioph (Poly.const n)

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

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

Разделы

Аффилиация

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