English
There is a natural Algebra structure of Laurent polynomials over the polynomial ring: LaurentPolynomial(R) is an Algebra over Polynomial(R), with algebraMap given by toLaurent and X commuting with the elements of Polynomial(R).
Русский
Существует натуральная алгебраическая структура лаурентовых полиномов над полиномами: LaurentPolynomial(R) является алгеброй над Polynomial(R), отображение алгебры задано через toLaurent и переменная X коммутирует с элементами Polynomial(R).
LaTeX
$$$\\text{Algebra}(\\mathrm{Polynomial}(R), \\mathrm{LaurentPolynomial}(R))$ with $\\text{algebraMap} = \\mathrm{toLaurent}$ and $X$ commuting.$$
Lean4
instance algebraPolynomial (R : Type*) [CommSemiring R] : Algebra R[X] R[T;T⁻¹]
where
algebraMap := Polynomial.toLaurent
commutes' := fun f l => by simp [mul_comm]
smul_def' := fun _ _ => rfl
