Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-27 11:31 efeeacaf

View on Github →

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.

Estimated changes