mathlib3

ce107da5 - feat(analysis/special_functions/integrals): integrating linear combinations of functions (#6597)

feat(analysis/special_functions/integrals): integrating linear combinations of functions (#6597) Together with #6357, this PR makes it possible to compute integrals of the form `∫ x in a..b, c * f x + d * g x` by `simp` (where `c` and `d` are constants and `f` and `g` are functions that are `interval_integrable` on `interval a b`. Notably, this allows us to compute the integrals of polynomials by `norm_num`. Here's an example, followed by an example of a more random linear combination of `interval_integrable` functions: ``` import analysis.special_functions.integrals open interval_integral real open_locale real example : ∫ x:ℝ in 0..2, 6*x^5 + 3*x^4 + x^3 - 2*x^2 + x - 7 = 1048 / 15 := by norm_num example : ∫ x:ℝ in 0..1, exp x + 9 * x^8 + x^3 - x/2 + (1 + x^2)⁻¹ = exp 1 + π/4 := by norm_num ```