mathlib

4ae5e7a0 - feat(data/polynomial/laurent): laurent polynomials are a module over polynomials (#14121)

feat(data/polynomial/laurent): laurent polynomials are a module over polynomials (#14121) This PR only introduces the instance `module R[X] R[T;T⁻¹]`. I isolated it from the rest, since I want to give special attention to whether there might be any issues declaring it a global instance and whether it should be localized or even simply a def. Edit: Eric seems happy with this instance!