mathlib

43379184 - feat(analysis/special_functions/integrals): integral of `sin x ^ m * cos x ^ n` (#7418)

feat(analysis/special_functions/integrals): integral of `sin x ^ m * cos x ^ n` (#7418) The simplification of integrals of the form `∫ x in a..b, sin x ^ m * cos x ^ n` where (i) `n` is odd, (ii) `m` is odd, and (iii) `m` and `n` are both even. The computation of the integrals of the following functions are then provided outright: - `sin x * cos x`, given both in terms of sine and cosine - `sin x ^ 2 * cos x ^ 2` - `sin x ^ 2 * cos x` and `sin x * cos x ^ 2` - `sin x ^ 3` and `cos x ^ 3`