Commit 2022-09-29 01:02 8f89631e
View on Github →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
.