Theorem DomMulAct.smul_Lp_zero

Modification history

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