mathlib

8f89631e - refactor(algebra/periodic): use `neg_zero_class` for `antiperiodic.nat_mul_eq_of_eq_zero` (#16687)

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