Commit 2025-05-11 06:30 f24b1dcf

View on Github →

chore(MeasureTheory): relax lots of typeclass assumptions (#24737) Generalise lots of theorems about scalar multiplication actions on integrals to allow normed rings, rather than normed fields.

Estimated changes

added theorem hasMellin_const_smul
modified theorem mellin_const_smul
modified theorem ContinuousMap.coeFn_toLp
modified theorem ContinuousMap.coe_toLp
modified theorem ContinuousMap.range_toLp
modified def ContinuousMap.toLp
modified theorem ContinuousMap.toLp_def
modified theorem ContinuousMap.toLp_inj
modified theorem MeasureTheory.integral_smul
modified theorem IntervalIntegrable.smul
modified theorem MeasureTheory.setToFun_smul