aeval_fn_apply

Mathlib.Algebra.Polynomial.AlgebraMap

URI: https://scilib.ai/kg/mathlib#Polynomial.aeval_fn_apply

← MathLib Explorer

English

Same as previous: ((aeval f) g) x = aeval (f x) g for all x, g, f.

Русский

То же самое: ((aeval f) g) x = aeval (f x) g для любых x, g, f.

LaTeX

$$$(g : R[X]) \; (f : X \to R) \; (x : X):\; ((\operatorname{aeval} f) g) x = \operatorname{aeval}(f(x)) g.$$$

Lean4

@[simp]
theorem aeval_fn_apply {X : Type*} (g : R[X]) (f : X → R) (x : X) : ((aeval f) g) x = aeval (f x) g :=
  (aeval_algHom_apply (Pi.evalAlgHom R (fun _ => R) x) f g).symm

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

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

Разделы

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

Аффилиация

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