mathlib3

a4211857 - feat(algebra/periodic): more periodicity lemmas (#7853)