refactor(algebra/periodic): weaken another antiperiodic typeclass a…

…ssumption (#15961)

Followup to #15941 and #15782, weakening the typeclass assumption on
the codomain of the antiperiodic function in `antiperiodic.const_sub`
(added by #15782) in the same way as done for other lemmas in #15941.

src/algebra/periodic.lean

@@ -456,7 +456,8 @@ lemma antiperiodic.add_const [add_comm_semigroup α] [has_neg β] (h : antiperio
   antiperiodic (λ x, f (x + a)) c :=
 λ x, by simpa [add_assoc x c a, add_comm c, ←add_assoc x a c] using h (x + a)
 
-lemma antiperiodic.const_sub [add_comm_group α] [add_group β] (h : antiperiodic f c) (a : α) :
+lemma antiperiodic.const_sub [add_comm_group α] [has_involutive_neg β] (h : antiperiodic f c)
+  (a : α) :
   antiperiodic (λ x, f (a - x)) c :=
 begin
   rw [←neg_neg c],