Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-11 11:13 c500b99f

View on Github →

feat(ring_theory/laurent): coe from R[[x]] to R((x)) (#11318) And actually the changes reported in #11295 Generalize power_series.coeff_smul

Estimated changes

deleted theorem polynomial.coe_coe
deleted theorem polynomial.coe_laurent
deleted theorem polynomial.coe_laurent_C
deleted theorem polynomial.coe_laurent_X
added theorem power_series.coe_C
added theorem power_series.coe_X
added theorem power_series.coe_add
added theorem power_series.coe_bit0
added theorem power_series.coe_bit1
added theorem power_series.coe_mul
added theorem power_series.coe_one
added theorem power_series.coe_pow
added theorem power_series.coe_smul
added theorem power_series.coe_zero
added theorem power_series.coeff_coe
modified theorem power_series.coeff_smul