eval₂_mul_C — Mathlib

English

Evaluating a product of a polynomial with a monomial yields a product formula involving p, a, and the monomial's support.

Русский

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

LaTeX

$$$\forall {s,a}, (p \cdot \operatorname{monomial}(s)\; a).eval₂ f g = p.eval₂ f g \cdot f(a) \cdot s.prod_{n,e} (g(n))^e$$$

Lean4

theorem eval₂_mul_C : (p * C a).eval₂ f g = p.eval₂ f g * f a :=
  (eval₂_mul_monomial _ _).trans <| by simp

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