mathlib3

4a8ce41e - feat(analysis/special_functions/trigonometric): facts about periodic trigonometric functions (#7841)

feat(analysis/special_functions/trigonometric): facts about periodic trigonometric functions (#7841) I use the periodicity API that I added in #7572 to write lemmas about sine (real and complex), cosine (real and complex), tangent (real and complex), and the exponential function (complex only).