algEquivCMulXAddC_symm_eq — Mathlib

English

If a is invertible, the inverse of the automorphism φ_{a,b} (p(X) → p(aX + b)) is the automorphism with parameters a^{-1} and −a^{-1}b, i.e., φ_{a,b}^{-1} = φ_{a^{-1}, −a^{-1}b}.

Русский

Если a обратимо, обратный автоморфизм к φ_{a,b} (p(X) → p(aX + b)) равен автоморфизму с параметрами a^{-1} и −a^{-1}b, то есть φ_{a,b}^{-1} = φ_{a^{-1}, −a^{-1}b}.

LaTeX

$$$\left(\operatorname{algEquivCMulXAddC}(a,b)\right)^{-1} = \operatorname{algEquivCMulXAddC}(a^{-1}, -a^{-1}b).$$$

Lean4

theorem algEquivCMulXAddC_symm_eq {R : Type*} [CommRing R] (a b : R) [Invertible a] :
    (algEquivCMulXAddC a b).symm = algEquivCMulXAddC (⅟a) (-⅟a * b) :=
  by
  ext p : 1
  simp only [algEquivCMulXAddC_symm_apply, neg_mul, algEquivCMulXAddC_apply, map_neg, map_mul]
  congr
  simp [mul_add, sub_eq_add_neg]

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