English
Let R be a commutative ring and a ∈ R be invertible with b ∈ R. Then there exists an R-algebra automorphism φ of the polynomial ring R[X] that sends X to aX + b; its inverse sends X to a^{-1}(X − b). In particular, φ(p) = p(aX + b).
Русский
Пусть R — коммутативное кольцо, a ∈ R обратим и b ∈ R. Существует автоморфизм R[X]-алгебр над R, который отображает X в aX + b; обратный автоморфизм отображает X в a^{-1}(X − b). В частности, φ(p) = p(aX + b).
LaTeX
$$$\exists \phi \in \mathrm{Aut}_R(R[X]),\quad \phi(p) = p(aX + b) \ \forall p \in R[X], \text{ and }\; \phi^{-1}(X) = a^{-1}(X - b).$$$
Lean4
/-- The automorphism of the polynomial algebra given by `p(X) ↦ p(a * X + b)`,
with inverse `p(X) ↦ p(a⁻¹ * (X - b))`. -/
@[simps!]
def algEquivCMulXAddC {R : Type*} [CommRing R] (a b : R) [Invertible a] : R[X] ≃ₐ[R] R[X] :=
algEquivOfCompEqX (C a * X + C b) (C ⅟a * (X - C b)) (by simp [← C_mul, ← mul_assoc]) (by simp [← C_mul, ← mul_assoc])
