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.

src/ring_theory/hahn_series.lean

@@ -1159,7 +1159,7 @@ end algebra
 
 section valuation
 
-variables (Γ R) [linear_ordered_add_comm_group Γ] [ring R] [is_domain R]
+variables (Γ R) [linear_ordered_cancel_add_comm_monoid Γ] [ring R] [is_domain R]
 
 /-- The additive valuation on `hahn_series Γ R`, returning the smallest index at which
   a Hahn Series has a nonzero coefficient, or `⊤` for the 0 series.  -/
@@ -1208,7 +1208,7 @@ end
 end valuation
 
 lemma is_pwo_Union_support_powers
-  [linear_ordered_add_comm_group Γ] [ring R] [is_domain R]
+  [linear_ordered_cancel_add_comm_monoid Γ] [ring R] [is_domain R]
   {x : hahn_series Γ R} (hx : 0 < add_val Γ R x) :
   (⋃ n : ℕ, (x ^ n).support).is_pwo :=
 begin
@@ -1531,7 +1531,7 @@ end emb_domain
 
 section powers
 
-variables [linear_ordered_add_comm_group Γ] [comm_ring R] [is_domain R]
+variables [linear_ordered_cancel_add_comm_monoid Γ] [comm_ring R] [is_domain R]
 
 /-- The powers of an element of positive valuation form a summable family. -/
 def powers (x : hahn_series Γ R) (hx : 0 < add_val Γ R x) :