refactor(algebra/periodic): weaken antiperiodic typeclass assumptio…

…ns (#15941)

Many lemmas about `antiperiodic` have typeclass assumptions on the
codomain of the antiperiodic function that are stronger than
necessary, generally because the weaker typeclasses didn't exist when
most of the lemmas were added.  Weaken those assumptions as follows:

* `add_group` to `has_involutive_neg` (the most common change).
* `add_group` to `has_neg` (in a few places).
* `add_group` to `subtraction_monoid` (twice).
* `ring` to `has_mul` with `has_distrib_neg` (once).
* `division_ring` to `division_monoid` with `has_distrib_neg` (once).

There remain three cases where lemmas have typeclass assumptions
requiring addition and subtraction operations on the codomain, despite
those operations not otherwise being used in the lemma, because of the
lack of more specific typeclasses appropriate to those lemmas.  The
two that I changed to use `subtraction_monoid` actually only need the
`neg_zero` lemma (along with `has_involutive_neg` in one case), but we
don't have a typeclass for types that satisfy `neg_zero` (one example
without addition and subtraction operations is `sign_type`).  And
`antiperiodic.smul` actually only needs a scalar action that satisfies
`smul_neg`, without needing addition or subtraction operations on the
type on which the scalar action acts, but again we don't have such a
typeclass (and I don't know if we have any such scalar actions in
mathlib for which such a typeclass would actually enable this lemma to
apply).

src/algebra/periodic.lean

@@ -372,14 +372,14 @@ lemma antiperiodic.funext [has_add α] [has_neg β]
   (λ x, f (x + c)) = -f :=
 funext h
 
-lemma antiperiodic.funext' [has_add α] [add_group β]
+lemma antiperiodic.funext' [has_add α] [has_involutive_neg β]
   (h : antiperiodic f c) :
   (λ x, -f (x + c)) = f :=
 (eq_neg_iff_eq_neg.mp h.funext).symm
 
 /-- If a function is `antiperiodic` with antiperiod `c`, then it is also `periodic` with period
   `2 * c`. -/
-lemma antiperiodic.periodic [semiring α] [add_group β]
+lemma antiperiodic.periodic [semiring α] [has_involutive_neg β]
   (h : antiperiodic f c) :
   periodic f (2 * c) :=
 by simp [two_mul, ← add_assoc, h _]
@@ -388,27 +388,27 @@ lemma antiperiodic.eq [add_zero_class α] [has_neg β]
   (h : antiperiodic f c) : f c = -f 0 :=
 by simpa only [zero_add] using h 0
 
-lemma antiperiodic.nat_even_mul_periodic [semiring α] [add_group β]
+lemma antiperiodic.nat_even_mul_periodic [semiring α] [has_involutive_neg β]
   (h : antiperiodic f c) (n : ℕ) :
   periodic f (n * (2 * c)) :=
 h.periodic.nat_mul n
 
-lemma antiperiodic.nat_odd_mul_antiperiodic [semiring α] [add_group β]
+lemma antiperiodic.nat_odd_mul_antiperiodic [semiring α] [has_involutive_neg β]
   (h : antiperiodic f c) (n : ℕ) :
   antiperiodic f (n * (2 * c) + c) :=
 λ x, by rw [← add_assoc, h, h.periodic.nat_mul]
 
-lemma antiperiodic.int_even_mul_periodic [ring α] [add_group β]
+lemma antiperiodic.int_even_mul_periodic [ring α] [has_involutive_neg β]
   (h : antiperiodic f c) (n : ℤ) :
   periodic f (n * (2 * c)) :=
 h.periodic.int_mul n
 
-lemma antiperiodic.int_odd_mul_antiperiodic [ring α] [add_group β]
+lemma antiperiodic.int_odd_mul_antiperiodic [ring α] [has_involutive_neg β]
   (h : antiperiodic f c) (n : ℤ) :
   antiperiodic f (n * (2 * c) + c) :=
 λ x, by rw [← add_assoc, h, h.periodic.int_mul]
 
-lemma antiperiodic.nat_mul_eq_of_eq_zero [comm_semiring α] [add_group β]
+lemma antiperiodic.nat_mul_eq_of_eq_zero [comm_semiring α] [subtraction_monoid β]
   (h : antiperiodic f c) (hi : f 0 = 0) (n : ℕ) :
   f (n * c) = 0 :=
 begin
@@ -418,7 +418,7 @@ begin
   { simpa [add_mul, hk, hi] using (h.nat_odd_mul_antiperiodic k).eq },
 end
 
-lemma antiperiodic.int_mul_eq_of_eq_zero [comm_ring α] [add_group β]
+lemma antiperiodic.int_mul_eq_of_eq_zero [comm_ring α] [subtraction_monoid β]
   (h : antiperiodic f c) (hi : f 0 = 0) (n : ℤ) :
   f (n * c) = 0 :=
 begin
@@ -428,22 +428,22 @@ begin
   { simpa [add_mul, hk, hi] using (h.int_odd_mul_antiperiodic k).eq },
 end
 
-lemma antiperiodic.sub_eq [add_group α] [add_group β]
+lemma antiperiodic.sub_eq [add_group α] [has_involutive_neg β]
   (h : antiperiodic f c) (x : α) :
   f (x - c) = -f x :=
 by simp only [eq_neg_iff_eq_neg.mp (h (x - c)), sub_add_cancel]
 
-lemma antiperiodic.sub_eq' [add_comm_group α] [add_group β]
+lemma antiperiodic.sub_eq' [add_comm_group α] [has_neg β]
   (h : antiperiodic f c) :
   f (c - x) = -f (-x) :=
 by simpa only [sub_eq_neg_add] using h (-x)
 
-lemma antiperiodic.neg [add_group α] [add_group β]
+lemma antiperiodic.neg [add_group α] [has_involutive_neg β]
   (h : antiperiodic f c) :
   antiperiodic f (-c) :=
 by simpa only [sub_eq_add_neg, antiperiodic] using h.sub_eq
 
-lemma antiperiodic.neg_eq [add_group α] [add_group β]
+lemma antiperiodic.neg_eq [add_group α] [has_involutive_neg β]
   (h : antiperiodic f c) :
   f (-c) = -f 0 :=
 by simpa only [zero_add] using h.neg 0
@@ -524,42 +524,42 @@ lemma antiperiodic.div_inv [division_ring α] [has_neg β]
   antiperiodic (λ x, f (x / a)) (c * a) :=
 by simpa only [div_eq_mul_inv] using h.mul_const_inv ha
 
-lemma antiperiodic.add [add_group α] [add_group β]
+lemma antiperiodic.add [add_group α] [has_involutive_neg β]
   (h1 : antiperiodic f c₁) (h2 : antiperiodic f c₂) :
   periodic f (c₁ + c₂) :=
 by simp [*, ← add_assoc] at *
 
-lemma antiperiodic.sub [add_comm_group α] [add_group β]
+lemma antiperiodic.sub [add_comm_group α] [has_involutive_neg β]
   (h1 : antiperiodic f c₁) (h2 : antiperiodic f c₂) :
   periodic f (c₁ - c₂) :=
 let h := h2.neg in by simp [*, sub_eq_add_neg, add_comm c₁, ← add_assoc] at *
 
-lemma periodic.add_antiperiod [add_group α] [add_group β]
+lemma periodic.add_antiperiod [add_group α] [has_neg β]
   (h1 : periodic f c₁) (h2 : antiperiodic f c₂) :
   antiperiodic f (c₁ + c₂) :=
 by simp [*, ← add_assoc] at *
 
-lemma periodic.sub_antiperiod [add_comm_group α] [add_group β]
+lemma periodic.sub_antiperiod [add_comm_group α] [has_involutive_neg β]
   (h1 : periodic f c₁) (h2 : antiperiodic f c₂) :
   antiperiodic f (c₁ - c₂) :=
 let h := h2.neg in by simp [*, sub_eq_add_neg, add_comm c₁, ← add_assoc] at *
 
-lemma periodic.add_antiperiod_eq [add_group α] [add_group β]
+lemma periodic.add_antiperiod_eq [add_group α] [has_neg β]
   (h1 : periodic f c₁) (h2 : antiperiodic f c₂) :
   f (c₁ + c₂) = -f 0 :=
 (h1.add_antiperiod h2).eq
 
-lemma periodic.sub_antiperiod_eq [add_comm_group α] [add_group β]
+lemma periodic.sub_antiperiod_eq [add_comm_group α] [has_involutive_neg β]
   (h1 : periodic f c₁) (h2 : antiperiodic f c₂) :
   f (c₁ - c₂) = -f 0 :=
 (h1.sub_antiperiod h2).eq
 
-lemma antiperiodic.mul [has_add α] [ring β]
+lemma antiperiodic.mul [has_add α] [has_mul β] [has_distrib_neg β]
   (hf : antiperiodic f c) (hg : antiperiodic g c) :
   periodic (f * g) c :=
 by simp * at *
 
-lemma antiperiodic.div [has_add α] [division_ring β]
+lemma antiperiodic.div [has_add α] [division_monoid β] [has_distrib_neg β]
   (hf : antiperiodic f c) (hg : antiperiodic g c) :
   periodic (f / g) c :=
 by simp [*, neg_div_neg_eq] at *