Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-14 18:40 98c483b9

View on Github →

feat(ring_theory/hahn_series): a finsupp of Hahn series is a summable_family (#7091) Defines summable_family.of_finsupp

Estimated changes

Modified src/order/well_founded_set.lean

added theorem finset.is_wf_sup

Modified src/ring_theory/hahn_series.lean

modified def hahn_series.C

deleted theorem hahn_series.C_apply

added def hahn_series.coeff.add_monoid_hom

added def hahn_series.coeff.linear_map

modified def hahn_series.single.add_monoid_hom

deleted theorem hahn_series.single.add_monoid_hom_apply

modified def hahn_series.single.linear_map

deleted theorem hahn_series.single.linear_map_apply

added theorem hahn_series.summable_family.co_support_of_finsupp

added theorem hahn_series.summable_family.coe_of_finsupp

added theorem hahn_series.summable_family.hsum_of_finsupp

modified def hahn_series.summable_family.lsum

deleted theorem hahn_series.summable_family.lsum_apply

added def hahn_series.summable_family.of_finsupp

modified def hahn_series.to_power_series

modified def hahn_series.to_power_series_alg

deleted theorem hahn_series.to_power_series_alg_apply

deleted theorem hahn_series.to_power_series_alg_symm_apply