mathlib

ccf84e0d - feat(analysis/special_functions/trigonometric/series): express `cos`/`sin` as infinite sums (#18352)

feat(analysis/special_functions/trigonometric/series): express `cos`/`sin` as infinite sums (#18352) I wasn't able to find a nice way to prove this with `has_sum.even_add_odd`, so instead I transported across `nat.div_mod_equiv` such that I could split even and odd terms. If nothing else, this provides a nice example of how to use similar equivs to split by remainders upon division by values other than 2. [Zulip](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/real.2Ecos.20and.20real.2Esin.20as.20infinite.20series/near/325193524) Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>