Commit 2021-05-31 15:49 d0ebc8ef

View on Github →

feat(ring_theory/laurent_series): Defines Laurent series and their localization map (#7604) Defines laurent_series as an abbreviation of hahn_series Z Defines laurent_series.power_series_part Shows that the map from power series to Laurent series is a localization_map.

Estimated changes

Modified src/ring_theory/hahn_series.lean

modified def hahn_series.of_power_series

added theorem hahn_series.of_power_series_apply

added theorem hahn_series.of_power_series_apply_coeff

added theorem hahn_series.of_power_series_injective

Created src/ring_theory/laurent_series.lean

added theorem laurent_series.coe_power_series

added theorem laurent_series.coeff_coe_power_series

added theorem laurent_series.of_power_series_X

added theorem laurent_series.of_power_series_X_pow

added def laurent_series.of_power_series_localization

added theorem laurent_series.of_power_series_power_series_part

added def laurent_series.power_series_part

added theorem laurent_series.power_series_part_coeff

added theorem laurent_series.power_series_part_eq_zero

added theorem laurent_series.power_series_part_zero

added theorem laurent_series.single_order_mul_power_series_part

added def laurent_series