Commit 2025-04-07 16:44 8256881c

View on Github →

chore(MeasureTheory): generalize some smul lemmas (#23736) Allow scalar multiplication by scalars of other types (e.g., ℝ≥0∞, ℝ≥0, ℕ).

Estimated changes

Modified Mathlib/Analysis/FunctionalSpaces/SobolevInequality.lean

Modified Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean

Modified Mathlib/MeasureTheory/Function/SimpleFunc.lean

modified theorem MeasureTheory.SimpleFunc.lintegral_smul

Modified Mathlib/MeasureTheory/Integral/Average.lean

Modified Mathlib/MeasureTheory/Integral/Lebesgue.lean

modified theorem MeasureTheory.lintegral_smul_measure

modified theorem MeasureTheory.setLIntegral_smul_measure

Modified Mathlib/MeasureTheory/Measure/Restrict.lean

modified theorem MeasureTheory.Measure.restrict_smul

Modified Mathlib/MeasureTheory/Measure/WithDensity.lean

Modified Mathlib/Probability/Kernel/Disintegration/Basic.lean