mathlib3

d812abd8 - refactor(algebra/periodic): weaken `antiperiodic` typeclass assumptions (#15941)

refactor(algebra/periodic): weaken `antiperiodic` typeclass assumptions (#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).