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 `ℤ`.





leanprover-community/mathlib,leanprover-community/mathlib