invert — Mathlib

English

There is an algebra equivalence invert: LaurentPolynomial(R) ≃ₐ[R] LaurentPolynomial(R) which sends T to T^{-1}.

Русский

Существует алгебраическое эквивалентное отображение invert: LaurentPolynomial(R) ≃ₐ[R] LaurentPolynomial(R), которое переводит T в T^{-1}.

LaTeX

$$$\\text{invert}: \\mathrm{LaurentPolynomial}(R) \\to \\mathrm{LaurentPolynomial}(R) \\text{ is an algebra isomorphism with } \\text{invert}(T)=T^{-1}.$$$

Lean4

/-- The map which substitutes `T ↦ T⁻¹` into a Laurent polynomial. -/
def invert : R[T;T⁻¹] ≃ₐ[R] R[T;T⁻¹] :=
  AddMonoidAlgebra.domCongr R R <| AddEquiv.neg _

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