Commit 2025-09-23 12:05 45960ed5

View on Github →

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

Estimated changes

Modified Mathlib/MeasureTheory/Group/Convolution.lean

added theorem MeasureTheory.Measure.mconv_smul_left

Modified Mathlib/MeasureTheory/Measure/WithDensity.lean

added theorem MeasureTheory.Measure.mconv_smul_right