Commit 2025-04-23 20:46 b000f0cb

View on Github →

feat: MeasurableConstSMul (#24317) This typeclass will be useful in #23603.

Estimated changes

Modified Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean

Modified Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean

Modified Mathlib/MeasureTheory/Group/Arithmetic.lean

deleted theorem AEMeasurable.const_smul'

modified theorem AEMeasurable.const_smul

added theorem AEMeasurable.fun_const_smul

deleted theorem Measurable.const_smul'

modified theorem Measurable.const_smul

added theorem Measurable.fun_const_smul

Modified Mathlib/MeasureTheory/Group/MeasurableEquiv.lean

Modified Mathlib/MeasureTheory/Group/Measure.lean

Modified Mathlib/MeasureTheory/Integral/Bochner/Basic.lean

Modified Mathlib/MeasureTheory/Measure/Haar/Unique.lean

Modified Mathlib/MeasureTheory/Measure/Regular.lean