Theorem MeasureTheory.Measure.mconv_smul_left

Modification history

2025-09-23 12:05

Mathlib/MeasureTheory/Group/Convolution.lean

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

Added MeasureTheory.Measure.mconv_smul_left View on Github →