mathlib3

81c98d5b - feat(ring_theory/hahn_series): Hahn series form a field (#7495)

feat(ring_theory/hahn_series): Hahn series form a field (#7495) Uses Higman's Lemma to define `summable_family.powers`, a summable family consisting of the powers of a Hahn series of positive valuation Uses `summable_family.powers` to define inversion on Hahn series over a field and linear-ordered value group, making the type of Hahn series a field. Shows that a Hahn series over an integral domain and linear-ordered value group `is_unit` if and only if its lowest coefficient is.