mathlib

efeeacaf - feat(analysis/special_functions/integrals): integral of `sin x ^ n` (#7372)

feat(analysis/special_functions/integrals): integral of `sin x ^ n` (#7372) The reduction of `∫ x in a..b, sin x ^ n`, ∀ n ∈ ℕ, 2 ≤ n. We had this for the integral over [0, π] but I don't see any reason not to generalize it to any [a, b]. This also allows for the derivation of the integral of `sin x ^ 2` as a special case.