Commit 2025-01-21 14:10 22d5b968

View on Github →

chore: rename zero_memℒp to Memℒp.zero (#20915) This better matches the naming convention and unlocks anonymous dot notation. Also make both lemmas simp. From my PhD (LeanCamCombi)

Estimated changes

Modified Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean

added theorem MeasureTheory.Memℒp.zero'

added theorem MeasureTheory.Memℒp.zero

deleted theorem MeasureTheory.zero_mem_ℒp'

deleted theorem MeasureTheory.zero_memℒp

Modified Mathlib/MeasureTheory/Function/LpSeminorm/TriangleInequality.lean

Modified Mathlib/MeasureTheory/Function/LpSpace.lean

Modified Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean

modified theorem MeasureTheory.Lp.simpleFunc.toLp_zero

Modified Mathlib/Probability/Process/Filtration.lean

Modified scripts/nolints_prime_decls.txt