Commit 2021-05-10 22:45 81c98d5b

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.