Commit 2021-03-20 21:36 31531531

View on Github →

feat(measure_theory/interval_integral): add integral_comp_mul_left (#6787) I need this lemma for my work toward making integrals computable by norm_num.

Estimated changes

Modified src/measure_theory/interval_integral.lean

modified theorem interval_integral.integral_comp_add_right

added theorem interval_integral.integral_comp_mul_left

modified theorem interval_integral.integral_comp_mul_right

modified theorem interval_integral.integral_comp_neg