polynomial_smul_apply'

Mathlib.RingTheory.Algebraic.Pi

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

← MathLib Explorer

English

A variant with SMul on S → T: (p • f) x = aeval x p • f x.

Русский

Вариант с действием SMul на S → T: (p • f) x = aeval x p · f x.

LaTeX

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

Lean4

@[simp]
theorem polynomial_smul_apply' [CommSemiring R] [Semiring S] [Algebra R S] [SMul S T] (p : R[X]) (f : S → T) (x : S) :
    (p • f) x = aeval x p • f x :=
  rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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