Commit 2021-04-07 02:18 758d3228

View on Github →

feat(measure_theory/interval_integral): make integral_comp lemmas computable by simp (#7010) A follow-up to #6795, enabling the computation of integrals of the form ∫ x in a..b, f (c * x + d) by simp, where f is a function whose integral is already in mathlib and c and d are any real constants such that c ≠ 0.

Estimated changes

Modified src/measure_theory/interval_integral.lean

modified theorem interval_integral.integral_comp_add_div

modified theorem interval_integral.integral_comp_add_mul

modified theorem interval_integral.integral_comp_add_right

modified theorem interval_integral.integral_comp_div

modified theorem interval_integral.integral_comp_div_add

modified theorem interval_integral.integral_comp_div_sub

modified theorem interval_integral.integral_comp_mul_add

modified theorem interval_integral.integral_comp_mul_left

modified theorem interval_integral.integral_comp_mul_right

modified theorem interval_integral.integral_comp_mul_sub

modified theorem interval_integral.integral_comp_sub_div

modified theorem interval_integral.integral_comp_sub_left

modified theorem interval_integral.integral_comp_sub_mul

modified theorem interval_integral.integral_comp_sub_right