mathlib3

c500b99f - feat(ring_theory/laurent): coe from R[[x]] to R((x)) (#11318)

feat(ring_theory/laurent): coe from R[[x]] to R((x)) (#11318) And actually the changes reported in #11295 Generalize `power_series.coeff_smul` Co-authored-by: Eric Wieser <wieser.eric@gmail.com>