const_apply

Mathlib.NumberTheory.Dioph

URI: https://scilib.ai/kg/mathlib#Poly.const_apply

English

The constant polynomial applied to any input x yields the same value n: const(n)(x) = n.

Русский

Постоянный полином при любом входе x даёт то же самое значение n: const(n)(x) = n.

LaTeX

$$$(\text{const}(n))(x) = n$$$

Lean4

@[simp]
theorem const_apply (n) (x : α → ℕ) : const n x = n :=
  rfl

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

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

Разделы

Аффилиация

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