mathlib

cb8faf79 - feat(ring_theory/hahn_series): Loosen definition of additive valuation (#17057)

feat(ring_theory/hahn_series): Loosen definition of additive valuation (#17057) The definitions and theorems realted to the additive valuation of Hahn series don't actually require the value group to be a group; just a cancellative monoid, as in the rest of the file. This came about while I was thinking about Bhargava's recent proof of van der Waerden's theorem and I wondered how hard proving, say, the irreducibility theorem would be in mathlib.