Theorem MeasureTheory.Measure.mconv_smul_left

Modification history

2026-08-26 08:21
Mathlib/MeasureTheory/Group/Convolution.lean
refactor: change the default value of `Measure.map` to a Dirac mass (#42322) …
Modified MeasureTheory.Measure.mconv_smul_leftView on Github →
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_leftView on Github →