eval₂_restriction — Mathlib

English

Evaluating a polynomial after restriction is equal to evaluating the restricted polynomial under a suitably composed homomorphism.

Русский

Оценивание многочлена после ограничения равно оцениванию ограниченного многочлена под соответствующим композиционным гомоморфизмом.

LaTeX

$$$\\mathrm{eval}_2 f x(p) = \\mathrm{eval}_2 (f \\circ \\mathrm{Subring.closure}(p.coeffs)) x (\\mathrm{restriction}(p))$$$

Lean4

theorem eval₂_restriction {p : R[X]} :
    eval₂ f x p = eval₂ (f.comp (Subring.subtype (Subring.closure (p.coeffs : Set R)))) x p.restriction := by
  simp only [eval₂_eq_sum, sum, support_restriction, ← @coeff_restriction _ _ p, RingHom.comp_apply,
    Subring.coe_subtype]

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