Commit 2023-05-24 01:45 b3b7e04d

View on Github →

feat: port RingTheory.LaurentSeries (#4283)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RingTheory/HahnSeries.lean

added theorem HahnSeries.ofPowerSeries_X_pow

deleted theorem HahnSeries.ofPowerSeries_x_pow

Created Mathlib/RingTheory/LaurentSeries.lean

added theorem LaurentSeries.coe_algebraMap

added theorem LaurentSeries.coeff_coe_powerSeries

added theorem LaurentSeries.ofPowerSeries_powerSeriesPart

added def LaurentSeries.powerSeriesPart

added theorem LaurentSeries.powerSeriesPart_coeff

added theorem LaurentSeries.powerSeriesPart_eq_zero

added theorem LaurentSeries.powerSeriesPart_zero

added theorem LaurentSeries.single_order_mul_powerSeriesPart

added theorem PowerSeries.coe_C

added theorem PowerSeries.coe_X

added theorem PowerSeries.coe_add

added theorem PowerSeries.coe_mul

added theorem PowerSeries.coe_neg

added theorem PowerSeries.coe_one

added theorem PowerSeries.coe_pow

added theorem PowerSeries.coe_smul

added theorem PowerSeries.coe_sub

added theorem PowerSeries.coe_zero

added theorem PowerSeries.coeff_coe