instModulePolynomial — Mathlib

English

Laurent polynomials R[T; T^{-1}] form a module over the polynomial ring R[X], via the natural map toLaurent from Polynomial R.

Русский

Лаурентовыe полиномы R[T; T^{-1}] образуют модуль над кольцом многочленов R[X] через естественное отображение toLaurent из Polynomial R.

LaTeX

$$$\\mathrm{LaurentPolynomial}(R) \\text{ is a module over } \\mathrm{Polynomial}(R) \\text{ via } \\mathrm{toLaurent}$.$$

Lean4

instance : Module R[X] R[T;T⁻¹] :=
  Module.compHom _ Polynomial.toLaurent

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