Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-07 20:26 5cfcb6a0

View on Github →

feat(ring_theory/hahn_series): order of a nonzero Hahn series, reindexing summable families (#7444) Defines hahn_series.order, the order of a nonzero Hahn series Restates add_val in terms of hahn_series.order Defines hahn_series.summable_family.emb_domain, reindexing a summable family using an embedding

Estimated changes

Modified src/algebra/big_operators/finprod.lean

added theorem finprod_dmem

added theorem finprod_emb_domain'

added theorem finprod_emb_domain

Modified src/ring_theory/hahn_series.lean

added theorem hahn_series.C_injective

added theorem hahn_series.C_ne_zero

added theorem hahn_series.add_val_le_of_coeff_ne_zero

deleted theorem hahn_series.coeff_min_ne_zero

added theorem hahn_series.coeff_order_ne_zero

added theorem hahn_series.min_order_le_order_add

deleted theorem hahn_series.mul_coeff_min_add_min

added theorem hahn_series.mul_coeff_order_add_order

added theorem hahn_series.ne_zero_of_coeff_ne_zero

added def hahn_series.order

added theorem hahn_series.order_C

added theorem hahn_series.order_le_of_coeff_ne_zero

added theorem hahn_series.order_mul

added theorem hahn_series.order_of_ne

added theorem hahn_series.order_one

added theorem hahn_series.order_single

added theorem hahn_series.order_zero

added theorem hahn_series.single_injective

added theorem hahn_series.single_ne_zero

added def hahn_series.summable_family.emb_domain

added theorem hahn_series.summable_family.emb_domain_apply

added theorem hahn_series.summable_family.emb_domain_image

added theorem hahn_series.summable_family.emb_domain_notin_range

added theorem hahn_series.summable_family.hsum_emb_domain

added theorem hahn_series.summable_family.hsum_sub