Commit 2022-09-29 01:02 8f89631e

refactor(algebra/periodic): use neg_zero_class for antiperiodic.nat_mul_eq_of_eq_zero (#16687) Weaken the typeclass assumption on the codomain of the antiperiodic function in antiperiodic.nat_mul_eq_of_eq_zero from subtraction_monoid to neg_zero_class. The corresponding int lemma also requires involutive neg so will be dealt with separately once we have a further typeclass for the combination of neg_zero_class with has_involutive_neg.