Commit 2022-08-09 12:53 d812abd8

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).