Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-23 09:38 ac712929

View on Github →

chore(measure_theory/integral): generalize integral_smul_const (#10411)

generalize to is_R_or_C;
add an interval_integral version.

Estimated changes

Modified src/analysis/special_functions/integrals.lean

deleted theorem interval_integral.integral_const_mul

deleted theorem interval_integral.integral_div

deleted theorem interval_integral.integral_mul_const

Modified src/measure_theory/function/conditional_expectation.lean

Modified src/measure_theory/integral/interval_integral.lean

added theorem interval_integral.integral_const_mul

added theorem interval_integral.integral_div

added theorem interval_integral.integral_mul_const

added theorem interval_integral.integral_smul_const

Modified src/measure_theory/integral/set_integral.lean

modified theorem integral_smul_const