refactor(RingTheory/HahnSeries) : several generalizations

[ScottCarnahan]

This PR is a container for several smaller PRs that refactor and generalize the existing Hahn series theory. It is (I think) all we need from Hahn series to get a palatable theory of vertex algebras off the ground (other prerequisites from Lie algebras will eventually come in a different PR). Major changes include:

• equivalence between iterated Hahn series and Hahn series on Lex products.
• introduce orderTop and leadingCoeff functions. Here, orderTop is a WithTop Γ-valued version of order that does not need [Zero Γ] and leadingCoeff returns the coefficient of the minimal element of support (or zero if empty).
• introduce ordered and cancellative vector addition classes together with some basic theory e.g., finiteness of antidiagonals for partially well-ordered sets.
• HahnSeries Γ R-module structure on HahnModule Γ' R V, when Γ is an OrderedCancelAddCommMonoid, Γ' is a PartialOrder with OrderedCancelVAdd Γ Γ', R is a semiring, and V is an R-module.
• Move AddVal to a separate file - the underlying function is just orderTop, but the description of the valuation needs an additional import and an IsDomain hypothesis. Results that depended on AddVal are changed to use orderTop and generalized.

---

• depends on: [Merged by Bors] - feat: HahnSeries on Lex product #10781 [HahnSeries on Lex product]
• depends on: [Merged by Bors] - feat (RingTheory/HahnSeries/Multiplication): module structure on HahnModule #10846 [HahnModule]
• depends on: [Merged by Bors] - feat (RingTheory/HahnSeries/Basic): define orderTop, taking values in WithTop #11965 [orderTop]
• depends on: [Merged by Bors] - feat (Algebra/Order/AddTorsor) : OrderedVAdd, OrderedCancelVAdd #11979 [OrderedVAdd]
• depends on: [Merged by Bors] - feat (RingTheory/HahnSeries) : def leadingCoeff, orderTop lemmas #12996 [leadingTerm]
• depends on: [Merged by Bors] - feat (RingTheory/HahnSeries/Summable) : coeff function for a summable family #16649
• depends on: [Merged by Bors] - feat (RingTheory/HahnSeries/Summable) : Pointwise SMul for summable families #16701
• depends on: [Merged by Bors] - feat (Data/Finset/Basic) : Equivalence between Pi type over Finset.cons and a product #17004

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat: HahnSeries on Lex product #10781
• [Merged by Bors] - feat (RingTheory/HahnSeries/Multiplication): module structure on HahnModule #10846
• [Merged by Bors] - feat (RingTheory/HahnSeries/Basic): define orderTop, taking values in WithTop #11965
• [Merged by Bors] - feat (Algebra/Order/AddTorsor) : OrderedVAdd, OrderedCancelVAdd #11979
• [Merged by Bors] - feat (RingTheory/HahnSeries) : def leadingCoeff, orderTop lemmas #12996
• [Merged by Bors] - feat (RingTheory/HahnSeries/Summable) : coeff function for a summable family #16649
• [Merged by Bors] - feat (RingTheory/HahnSeries/Summable) : Pointwise SMul for summable families #16701
• [Merged by Bors] - feat (Data/Finset/Basic) : Equivalence between Pi type over Finset.cons and a product #17004
  By Dependent Issues (🤖). Happy coding!