Theorem MeasureTheory.LpAddConst_zero

Modification history

2026-04-15 17:10
Mathlib/MeasureTheory/Function/LpSeminorm/TriangleInequality.lean
feat(MeasureTheory/LpSeminorm): add `rpow_add_le_mul_rpow_add_rpow'` variants (#37547) …
Deleted MeasureTheory.LpAddConst_zeroView on Github →
2024-02-06 02:47
Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
chore(LpSeminorm): further split the file (#10207)
Modified MeasureTheory.LpAddConst_zeroView on Github →
2023-05-28 20:07
Mathlib/MeasureTheory/Function/LpSeminorm.lean
feat: port MeasureTheory.Function.LpSeminorm (#4445)
Added MeasureTheory.LpAddConst_zeroView on Github →