eval_add — Mathlib

English

Let f: σ → R be a fixed evaluation. For polynomials p and q in MvPolynomial σ R, evaluation distributes over addition: eval f(p + q) = eval f(p) + eval f(q).

Русский

Пусть f: σ → R задаёт вычисление. Для полиномов p, q выполнено: eval f(p + q) = eval f(p) + eval f(q).

LaTeX

$$$$\operatorname{eval}_f(p + q) = \operatorname{eval}_f(p) + \operatorname{eval}_f(q).$$$$

Lean4

theorem eval_add : eval f (p + q) = eval f p + eval f q :=
  eval₂_add _ _

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