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.







leanprover-community/mathlib,leanprover-community/mathlib