Theorem MeasureTheory.AEEqFun.eLpNorm_star

Modification history

2026-02-04 08:49
Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
refactor(MeasureTheory/Function/LpSeminorm): split long file (#34813) …
Modified MeasureTheory.AEEqFun.eLpNorm_starView on Github →
2025-08-29 01:08
Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
feat(MeasureTheory): add `Star`, `InvolutiveStar`, and `TrivialStar` instances for `Lp` (#28410) …
Added MeasureTheory.AEEqFun.eLpNorm_starView on Github →