map_neg — Mathlib

English

Let f: R →+* S be a ring homomorphism and p a polynomial over R. Then Polynomial.map f of the negation of p equals the negation of Polynomial.map f applied to p.

Русский

Пусть f: R →+* S — кольцевое отображение и p полином над R. Тогда Polynomial.map f (−p) = − Polynomial.map f(p).

LaTeX

$$$Polynomial.map\\ f\\ (-p) = -Polynomial.map\\ f\\ p$$$

Lean4

@[simp]
protected theorem map_neg {S} [Ring S] (f : R →+* S) : (-p).map f = -p.map f :=
  (mapRingHom f).map_neg p

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