Commit 2021-04-07 06:34 21a96ef0

View on Github →

feat(ring_theory/hahn_series): summable families of Hahn series (#6997) Defines hahn_series.summable_family Defines the formal sum hahn_series.summable_family.hsum and its linear map version, hahn_series.summable_family.lsum

Estimated changes

Modified src/ring_theory/hahn_series.lean

added theorem hahn_series.summable_family.add_apply

added theorem hahn_series.summable_family.co_support_add_subset

added theorem hahn_series.summable_family.coe_add

added theorem hahn_series.summable_family.coe_injective

added theorem hahn_series.summable_family.coe_neg

added theorem hahn_series.summable_family.coe_sub

added theorem hahn_series.summable_family.coe_zero

added theorem hahn_series.summable_family.ext

added def hahn_series.summable_family.hsum

added theorem hahn_series.summable_family.hsum_add

added theorem hahn_series.summable_family.hsum_coeff

added theorem hahn_series.summable_family.hsum_smul

added theorem hahn_series.summable_family.is_wf_Union_support

added def hahn_series.summable_family.lsum

added theorem hahn_series.summable_family.lsum_apply

added theorem hahn_series.summable_family.mem_co_support

added theorem hahn_series.summable_family.neg_apply

added theorem hahn_series.summable_family.smul_apply

added theorem hahn_series.summable_family.sub_apply

added theorem hahn_series.summable_family.support_hsum_subset

added theorem hahn_series.summable_family.zero_apply

added structure hahn_series.summable_family