Commit 2026-01-07 11:50 e1462b59

View on Github →

feat(MeasureTheory): more MeasurableSMul -> MeasurableConstSMul (#33710)

Estimated changes

Modified Mathlib/MeasureTheory/Function/AEEqFun/DomAct.lean

Modified Mathlib/MeasureTheory/Function/LpSpace/DomAct/Basic.lean

Modified Mathlib/MeasureTheory/Group/Arithmetic.lean

Modified Mathlib/MeasureTheory/Group/FundamentalDomain.lean

modified theorem MeasureTheory.IsFundamentalDomain.quotientMeasure_eq

modified theorem MeasureTheory.IsFundamentalDomain.smul_of_comm

Modified Mathlib/MeasureTheory/Group/Integral.lean

Modified Mathlib/MeasureTheory/Group/Measure.lean

Modified Mathlib/MeasureTheory/Group/Pointwise.lean

modified theorem MeasurableSet.const_smul