Theorem MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm_toReal

Modification history

2026-02-09 07:29
Mathlib/MeasureTheory/Function/LpSeminorm/Defs.lean
feat: real-valued Lᵖ norm (#23881)
Added MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm_toRealView on Github →