algEquivAevalNegX — Mathlib

English

There exists an involutive automorphism of R[X] sending X to −X, i.e., p(X) ↦ p(−X).

Русский

Существует инволютивный автоморфизм R[X], отправляющий X в −X, то есть p(X) ↦ p(−X).

LaTeX

$$$\exists \psi \in \mathrm{Aut}_R(R[X]),\quad \psi(X) = -X,\; \psi(p) = p(-X).$$$

Lean4

/-- The involutive automorphism of the polynomial algebra given by `p(X) ↦ p(-X)`. -/
@[simps!]
def algEquivAevalNegX {R : Type*} [CommRing R] : R[X] ≃ₐ[R] R[X] :=
  algEquivOfCompEqX (-X) (-X) (by simp) (by simp)

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