toLaurentAlg — Mathlib

English

The algebra map to Laurent polynomials, when applied to a polynomial p, coincides with the Laurent map on p.

Русский

Картa алгебры к лорантовым полиномам, примененная к полиному p, совпадает с лорантовой картой на p.

LaTeX

$$$\\text{toLaurentAlg}(p) = \\text{toLaurent}(p)$$$

Lean4

/-- The `R`-algebra map, taking a polynomial with coefficients in `R` to a Laurent polynomial
with coefficients in `R`. -/
def toLaurentAlg [CommSemiring R] : R[X] →ₐ[R] R[T;T⁻¹] :=
  (mapDomainAlgHom R R Int.ofNatHom).comp (toFinsuppIsoAlg R).toAlgHom

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