English
There exists a natural truncation map from Laurent polynomials to ordinary polynomials which keeps only the nonnegative-degree terms, and this truncation is a left inverse to the Laurent-to-polynomial embedding.
Русский
Существуют усечения Лоурента, отображающие лоурентовые многочлены в обычные полиномы, сохраняя только члены неотрицательной степени; такое усечение является левым обратным вложению в отображение полиномов в лаурентовые полиномы.
LaTeX
$$$\text{trunc} : R[T;T^{-1}] \to R[X], \quad \text{toLaurent} : R[X] \to R[T;T^{-1}], \quad \text{trunc} \circ \text{toLaurent} = \mathrm{id}_{R[X]}$$$
Lean4
/-- `trunc : R[T;T⁻¹] →+ R[X]` maps a Laurent polynomial `f` to the polynomial whose terms of
nonnegative degree coincide with the ones of `f`. The terms of negative degree of `f` "vanish".
`trunc` is a left-inverse to `Polynomial.toLaurent`. -/
def trunc : R[T;T⁻¹] →+ R[X] :=
(toFinsuppIso R).symm.toAddMonoidHom.comp <| comapDomain.addMonoidHom fun _ _ => Int.ofNat.inj
