hom_eval₂

Mathlib.Algebra.Polynomial.Eval.Coeff

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

English

If g: S →+* T and f: R →+* S are ring homs, then g( p.eval₂ f x ) = p.eval₂ (g ∘ f) (g x).

Русский

Если g: S →+* T и f: R →+* S — кольцевые гомоморфизмы, то g( p.eval₂ f x ) = p.eval₂ (g ∘ f) (g x).

LaTeX

$$$ g\\bigl(p.eval₂ f x\\bigr) = p.eval₂ (g \\circ f) (g x) $$$

Lean4

theorem hom_eval₂ (x : S) : g (p.eval₂ f x) = p.eval₂ (g.comp f) (g x) := by rw [← eval₂_map, eval₂_at_apply, eval_map]

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

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

Разделы

Аффилиация

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