Theorem MeasureTheory.MemLp.zero'

Modification history

2025-03-09 18:34

Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean

chore(MeasureTheory/Function/LpSeminorm/Basic): generalise more results to enorm classes (#22708) …

Modified MeasureTheory.MemLp.zero'View on Github →

2025-02-21 20:26

Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean

Rename `Mem𝓛p` to `MemLp` (#22164) …

Added MeasureTheory.MemLp.zero'View on Github →