eval₂_C

Mathlib.Algebra.Polynomial.Eval.Defs

URI: https://scilib.ai/kg/mathlib#Polynomial.eval₂_C

English

The evaluation of a constant polynomial C a under eval₂ yields f a.

Русский

Выражение константы полинома C a под eval₂ равно f a.

LaTeX

$$$ eval\\_2\\ f\\ x\\ (C\\ a) = f a $$$

Lean4

@[simp]
theorem eval₂_C : (C a).eval₂ f x = f a := by simp [eval₂_eq_sum]

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

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

Разделы

Аффилиация

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