Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-09 00:00 49cf3869

View on Github →

feat(measure_theory/measure/vector_measure): add absolutely_continuous.add and absolutely_continuous.smul (#9086)

Estimated changes

Modified src/measure_theory/measure/vector_measure.lean

added theorem measure_theory.vector_measure.absolutely_continuous.add

added theorem measure_theory.vector_measure.absolutely_continuous.neg_left

added theorem measure_theory.vector_measure.absolutely_continuous.neg_right

added theorem measure_theory.vector_measure.absolutely_continuous.smul

added theorem measure_theory.vector_measure.absolutely_continuous.sub