Def MeasureTheory.Lp.simpleFunc.toLp

Modification history

2024-05-07 01:05
Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean
refactor: replace `@[reducible]` with `abbrev` (#12614) …
Deleted MeasureTheory.Lp.simpleFunc.toLpView on Github →
2023-06-02 11:07
Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean
feat: port MeasureTheory.Function.SimpleFuncDenseLp (#4521)
Added MeasureTheory.Lp.simpleFunc.toLpView on Github →