mathlib3

9b41e4e0 - feat(data/polynomial/laurent): add truncation from Laurent polynomials to polynomials (#14085)

feat(data/polynomial/laurent): add truncation from Laurent polynomials to polynomials (#14085) We introduce the truncation of a Laurent polynomial `f`. It returns a polynomial whose support is exactly the non-negative support of `f`. We use it to prove injectivity of the inclusion of polynomials in Laurent polynomials. I also plan to use the results in this PR to prove that any Laurent polynomials is obtain from a polynomial by dividing by a power of the variable. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>