Theorem DomMulAct.mk_smul_toLp

Modification history

2025-02-21 20:26

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

Rename `Mem𝓛p` to `MemLp` (#22164) …

Modified DomMulAct.mk_smul_toLp View on Github →

2023-07-31 19:47

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

feat(MeasureTheory): define `DomMulAct` action on `Lp` (#6190)

Added DomMulAct.mk_smul_toLp View on Github →