Theorem DomMulAct.edist_smul_Lp

Modification history

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