eval₂_comp — Mathlib

English

For any RingHom f, polynomials p, q and x, eval₂ f x (p.comp q) = eval₂ f (eval₂ f x q) p.

Русский

Для кольцевого гомоморфа f, полиномов p, q и элемента x выполняется eval₂ f x (p.comp q) = eval₂ f (eval₂ f x q) p.

LaTeX

$$$\\operatorname{eval}_2 f x (p\\circ q) = \\operatorname{eval}_2 f (\\operatorname{eval}_2 f x q) p$$

Lean4

theorem eval₂_comp {x : S} : eval₂ f x (p.comp q) = eval₂ f (eval₂ f x q) p := by rw [comp, p.as_sum_range];
  simp [eval₂_finset_sum, eval₂_pow]

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