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