coe_aeval_eq_evalRingHom

Mathlib.Algebra.Polynomial.AlgebraMap

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

English

For g ∈ R[X], f : X → R, x ∈ X, ((aeval f) g) x = aeval (f x) g.

Русский

Для g ∈ R[X], f : X → R, x ∈ X выполняется ((aeval f) g) x = aeval (f x) g.

LaTeX

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

Lean4

@[simp]
theorem coe_aeval_eq_evalRingHom (x : R) : ((aeval x : R[X] →ₐ[R] R) : R[X] →+* R) = evalRingHom x :=
  rfl

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

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

Разделы

Аффилиация

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