mathlib3

5cfcb6a0 - feat(ring_theory/hahn_series): order of a nonzero Hahn series, reindexing summable families (#7444)

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