algEquivAevalXAddC_symm — Mathlib

English

The inverse of φ_t is φ_{-t}, i.e., (φ_t)^{-1} = φ_{-t} and hence maps X to X − t.

Русский

Обратный к φ_t автоморфизм равен φ_{-t}, то есть (φ_t)^{-1} = φ_{-t}, и он переносит X в X − t.

LaTeX

$$$(\operatorname{algEquivAevalXAddC}(t))^{-1} = \operatorname{algEquivAevalXAddC}(-t).$$$

Lean4

@[simp]
theorem algEquivAevalXAddC_symm {R : Type*} [CommRing R] (t : R) :
    (algEquivAevalXAddC t).symm = algEquivAevalXAddC (-t) := by simp [algEquivAevalXAddC, sub_eq_add_neg]

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