mapRingHom_comp_C

Mathlib.Algebra.Polynomial.Eval.Defs

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

English

For polynomials p, q, map f preserves composition: map f (p ∘ q) = (map f p) ∘ (map f q).

Русский

Отображение сохраняет композицию: map f (p ∘ q) = (map f p) ∘ (map f q).

LaTeX

$$$$\\operatorname{map} f (p.comp q) = (\\operatorname{map} f p).comp (\\operatorname{map} f q)$$$$

Lean4

theorem mapRingHom_comp_C {R S : Type*} [Semiring R] [Semiring S] (f : R →+* S) : (mapRingHom f).comp C = C.comp f := by
  ext; simp

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

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

Разделы

Аффилиация

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