algEquivAevalXAddC — Mathlib

English

For t ∈ R there is an R-algebra automorphism of R[X] sending X to X + t, with inverse sending X to X − t.

Русский

Для t ∈ R существует R-алгебр автоморфизм R[X], отправляющий X в X + t, а обратный отправляющий X в X − t.

LaTeX

$$$\exists \phi_t \in \mathrm{Aut}_R(R[X]),\quad \phi_t(X) = X + t, \text{ and } \phi_t^{-1}(X) = X - t.$$$

Lean4

/-- The automorphism of the polynomial algebra given by `p(X) ↦ p(X+t)`,
  with inverse `p(X) ↦ p(X-t)`. -/
@[simps!]
def algEquivAevalXAddC {R : Type*} [CommRing R] (t : R) : R[X] ≃ₐ[R] R[X] :=
  algEquivOfCompEqX (X + C t) (X - C t) (by simp) (by simp)

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