mathlib

fb72599b - feat(algebra/periodic): define periodicity (#7572)

feat(algebra/periodic): define periodicity (#7572) This PR introduces a general notion of periodicity. It also includes proofs of the "usual" properties of periodic (and antiperiodic) functions.