one_apply

Mathlib.NumberTheory.Dioph

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

English

The constant polynomial 1 evaluates to 1 at every input: for all a ∈ α, (1 : Poly α)(a) = 1.

Русский

Константный полином 1 принимает значение 1 при любом аргументе: для всякого a ∈ α выполняется (1 : Poly α)(a) = 1.

LaTeX

$$$$ (1 : Poly \\alpha)(a) = 1 $$$$

Lean4

@[simp]
theorem one_apply (x) : (1 : Poly α) x = 1 :=
  rfl

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

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

Разделы

Аффилиация

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