Theorem MeasureTheory.eLpNorm_ofReal

Modification history

2025-05-15 14:33
Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
chore(LpSeminorm/Basic): golf a norm lemma using its enorm equivalent (#24814) …
Added MeasureTheory.eLpNorm_ofRealView on Github →