mathlib3

954f3e16 - feat(algebra/periodic): `const_add`, `add_const`, `const_sub`, `sub_const` (#15782)

feat(algebra/periodic): `const_add`, `add_const`, `const_sub`, `sub_const` (#15782) Add lemmas that if `f` is periodic (or antiperiodic), so are functions such as `λ x, f (a + x)` and `λ x, f (x - a)` where a constant is added or subtracted on either side of the argument, with the same period. As far as I can tell, while mathlib has such lemmas about the effect of multiplying or dividing the argument by a constant on the period, it doesn't have them for addition or subtraction. It's possible some of these lemmas are true under weaker type class assumptions, though I think the type classes used are at least minimal for the proofs I used.