mathlib
ac712929 - chore(measure_theory/integral): generalize `integral_smul_const` (#10411)

Commit

4 years ago

chore(measure_theory/integral): generalize `integral_smul_const` (#10411) * generalize to `is_R_or_C`; * add an `interval_integral` version.

Author

urkud

Parents