eval₂_sub — Mathlib

English

Let f: R →+* S be a ring hom. For p, q ∈ R[X] and x ∈ S, the evaluation of p − q via eval₂ equals the difference of evaluations: (p − q).eval₂ f x = p.eval₂ f x − q.eval₂ f x.

Русский

Пусть f: R →+* S — кольцевое отображение. Для полиномов p, q ∈ R[X] и элемента x ∈ S выполняется eval₂ f x (p − q) = eval₂ f x p − eval₂ f x q.

LaTeX

$$$(p - q).eval_2\\ f\\ x = p.eval_2\\ f\\ x - q.eval_2\\ f\\ x$$$

Lean4

@[simp]
theorem eval₂_sub {S} [Ring S] (f : R →+* S) {x : S} : (p - q).eval₂ f x = p.eval₂ f x - q.eval₂ f x := by
  rw [sub_eq_add_neg, eval₂_add, eval₂_neg, sub_eq_add_neg]

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