Mathlib v3 is deprecated. Go to Mathlib v4

Theorem interval_integral.integral_const_mul

Modification history

2022-03-22 08:03
src/measure_theory/integral/interval_integral.lean
refactor(measure_theory/integral): restrict interval integrals to real intervals (#12754) …
Modified interval_integral.integral_const_mulView on Github →
2021-12-09 08:54
src/measure_theory/integral/interval_integral.lean
feat(topology/instances/real_vector_space): add an `is_scalar_tower` instance (#10490) …
Modified interval_integral.integral_const_mulView on Github →
2021-11-23 09:38
src/analysis/special_functions/integrals.lean
chore(measure_theory/integral): generalize `integral_smul_const` (#10411) …
Modified interval_integral.integral_const_mulView on Github →
2021-04-21 19:58
src/analysis/special_functions/integrals.lean
feat(analysis/special_functions/integrals): integral_comp for `f : ℝ → ℝ` (#7216) …
Modified interval_integral.integral_const_mulView on Github →
2021-03-07 03:26
src/analysis/special_functions/integrals.lean
feat(analysis/special_functions/integrals): mul/div by a const (#6357) …
Added interval_integral.integral_const_mulView on Github →