Mathlib v3 is deprecated. Go to Mathlib v4

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 .

Estimated changes