eval₂_add — Mathlib

English

Evaluation preserves addition: evaluating a sum of two polynomials equals the sum of their evaluations.

Русский

Оценивание сохраняет сложение: оценка суммы полиномов равна сумме их оценок.

LaTeX

$$$\\operatorname{ev}_{f,x}(p+q) = \\operatorname{ev}_{f,x}(p) + \\operatorname{ev}_{f,x}(q)$$$

Lean4

@[simp]
theorem eval₂_add : (p + q).eval₂ f x = p.eval₂ f x + q.eval₂ f x :=
  by
  simp only [eval₂_eq_sum]
  apply sum_add_index <;> simp [add_mul]

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