Mathlib v3 is deprecated. Go to Mathlib v4

Theorem measure_theory.vector_measure.mutually_singular.smul_left

Modification history

2022-02-18 04:52
src/measure_theory/measure/vector_measure.lean
feat(topology/algebra): generalize `has_continuous_smul` arguments to `has_continuous_const_smul` (#11999) …
Modified measure_theory.vector_measure.mutually_singular.smul_leftView on Github →
2021-09-10 07:18
src/measure_theory/measure/vector_measure.lean
feat(measure_theory/measure/vector_measure): define mutually singular for vector measures (#8896)
Added measure_theory.vector_measure.mutually_singular.smul_leftView on Github →