Theorem MeasureTheory.Lp.coeFn_star

Modification history

2025-08-29 01:08
Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
feat(MeasureTheory): add `Star`, `InvolutiveStar`, and `TrivialStar` instances for `Lp` (#28410) …
Added MeasureTheory.Lp.coeFn_starView on Github →