feat(ring_theory/laurent_series): introduce ring of Laurent series

[faenuccio]

Defines Laurent series
Provides basic algebraic structure on Laurent series, up to comm_ring, with still some sorry's left.

---

[bryangingechen]

Now that we have Hahn series, should the approach in this PR be modified? cc: @awainverse

[awainverse]

My inclination would be to define laurent_series R := hahn_series Z R, possibly as an abbreviation (I like abbreviations), and then use this PR as a checklist of API to add to that definition.

FWIW, I pretty much have a valuation on hahn_series (I believe it's up-to-date on the hahn_series2 branch) but it's an additive valuation, so I've gotten sidestepped into API for additive valuations. Once we have the valuation, it will be easier to describe summable series and use that to define inverses (you define inverses first for valuation-0 elements).

Certainly by the end of the process I described, we can add laurent_series, maybe earlier.

[faenuccio]

I certainly agree that this PR will need to be superseded by the approach we have on Hahn series, so I am converting it to a draft. In the meantime and before going to Laurent series as Hahn series on Z, it is worthwile, I believe, to see that power series (already in mathlib) are Hahn series on N. @awainverse : are you working on this? I'd be happy to do so, we can coordinate on Zulip.