Theorem MeasureTheory.MemLp.toLp_const

Modification history

2025-04-01 07:44

Mathlib/MeasureTheory/Function/LpSpace/Basic.lean

chore: split `MeasureTheory.Function.LpSpace.Basic` (#23508) …

Modified MeasureTheory.MemLp.toLp_const View on Github →

2025-02-21 20:26

Mathlib/MeasureTheory/Function/LpSpace/Basic.lean

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

Added MeasureTheory.MemLp.toLp_const View on Github →