Theorems · Definition · field theory

LaurentPolynomial.trunc

{R : Type u_1} → [inst : Semiring R] → LaurentPolynomial R →+ Polynomial R

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.

Defined in

Mathlib.Algebra.Polynomial.Laurent

Cited by

3 results in Mathlib

Foundations

Depth 89 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Semiring