Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-21 18:31 0c7ac835

View on Github →

feat(measure_theory/bochner_integration): add integral_smul_measure (#3900) Also add integral_dirac

Estimated changes

Modified src/measure_theory/bochner_integration.lean

modified theorem measure_theory.integral_add_measure

added theorem measure_theory.integral_dirac

added theorem measure_theory.integral_eq_zero_of_ae

added theorem measure_theory.integral_smul_measure

Modified src/measure_theory/measure_space.lean

added theorem measure_theory.ae_add_measure_iff

added theorem measure_theory.ae_smul_measure

added theorem measure_theory.measure.smul_apply