Theorem DomMulAct.smul_aeeqFun_const

Modification history

2023-07-31 19:47
Mathlib/MeasureTheory/Function/AEEqFun/DomAct.lean
feat(MeasureTheory): define `DomMulAct` action on `Lp` (#6190)
Added DomMulAct.smul_aeeqFun_constView on Github →