mathlib3

a484a7d0 - feat(ring_theory/hahn_series): add lemma neg_order (#18541)

feat(ring_theory/hahn_series): add lemma neg_order (#18541) added lemma `neg_order` stating that the order of the opposite of a Hahn series (with coefficients in an `add_group`) is the same of the order of the series itself.