Adding a notation for LaurentSeries

Stream: mathlib4

[Julian Berman]

Mathlib.RingTheory.PowerSeries.Basic defines (scoped) notation R⟦X⟧ for formal power series. Is a PR adding similar notation for Mathlib.RingTheory.LaurentSeries (which AIUI typically use R⸨X⸩) welcome?

A prerequisite is adding support for typing those doubled parens to vscode-lean4, which I'm about to do.

[Kevin Buzzard]

I would definitely be happy merging that!

[Julian Berman]

#16639