mathlib3

346174e9 - feat(data/polynomial/laurent): a Laurent polynomial can be multiplied by a power of `X` to "become" a polynomial (#14106)

feat(data/polynomial/laurent): a Laurent polynomial can be multiplied by a power of `X` to "become" a polynomial (#14106) This PR proves two versions of the result mentioned in the title, one involving multiplying by a non-negative power of `T`, the other usable as an induction principle.