Theorem ENNReal.LpAddConst_zero

Modification history

2026-04-15 17:10
Mathlib/Analysis/MeanInequalitiesPow.lean
feat(MeasureTheory/LpSeminorm): add `rpow_add_le_mul_rpow_add_rpow'` variants (#37547) …
Added ENNReal.LpAddConst_zeroView on Github →