eval₂_mul — Mathlib

English

Evaluating p multiplied by a constant C(a) reduces to q times the image of a under eval₂.

Русский

Оценка p умноженного на константу C(a) равно оценке p, умноженной на образ a.

LaTeX

$$$(p \cdot C a).eval₂ f g = p.eval₂ f g \cdot f a$$$

Lean4

@[simp]
theorem eval₂_mul : ∀ {p}, (p * q).eval₂ f g = p.eval₂ f g * q.eval₂ f g :=
  by
  apply MvPolynomial.induction_on q
  · simp [eval₂_C, eval₂_mul_C]
  · simp +contextual [mul_add, eval₂_add]
  · simp +contextual [X, eval₂_mul_monomial, ← mul_assoc]

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