Theorem MeasureTheory.Measure.mconv_smul_right

Modification history

2025-09-23 12:05

Mathlib/MeasureTheory/Measure/WithDensity.lean

feat(MeasureTheory): Add `mconv_smul_left` and `mconv_smul_right` (#29825)

Added MeasureTheory.Measure.mconv_smul_right View on Github →