eval₂_neg — Mathlib

English

Let f: R →+* S be a ring hom. For every p ∈ R[X] and every x ∈ S, the evaluation of −p via eval₂ equals the negation of the evaluation of p via eval₂.

Русский

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

LaTeX

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

Lean4

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

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