mathlib3

c76e1136 - feat(ring_theory/laurent): coercion of R[x] to R((x)) lemmas (#11295)

feat(ring_theory/laurent): coercion of R[x] to R((x)) lemmas (#11295) Make the coercion be `simp`-normal as opposed to `(algebra_map _ _)`. Also generalize `of_power_series Γ R (power_series.C R r) = hahn_series.C r` and similarly for `X` to be true for any `[ordered semiring Γ]`, not just `ℤ`.