comp_neg_X_comp_neg_X — Mathlib

English

Applying the substitution X ↦ −X twice yields the original polynomial: (p(−X))(−X) = p(X).

Русский

Двойное подстановление X↦−X возвращает исходный многочлен: (p(−X))^{(−X)} = p(X).

LaTeX

$$$(p\circ (-X))\circ (-X) = p$ for all polynomials p.$$

Lean4

theorem comp_neg_X_comp_neg_X {R : Type*} [CommRing R] (p : R[X]) : (p.comp (-X)).comp (-X) = p :=
  by
  rw [comp_assoc]
  simp only [neg_comp, X_comp, neg_neg, comp_X]

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