polynomial_smul_apply

Mathlib.RingTheory.Algebraic.Pi

URI: https://scilib.ai/kg/mathlib#polynomial_smul_apply

English

For p ∈ R[X], f ∈ R → S, x ∈ R we have (p • f)(x) = eval x p • f x.

Русский

Для p ∈ R[X], f ∈ R → S, x ∈ R выполняется (p • f)(x) = eval(x, p) · f(x).

LaTeX

$$$$ (p \cdot f)(x) = \operatorname{eval}(x, p) \cdot f(x). $$$$

Lean4

@[simp]
theorem polynomial_smul_apply [Semiring R] [SMul R S] (p : R[X]) (f : R → S) (x : R) : (p • f) x = eval x p • f x :=
  rfl

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

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

Разделы

Аффилиация

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