Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes