Commit 2022-01-08 16:29 c76e1136
View on Github →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 ℤ.