Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-14 23:07 d1904fce

View on Github →

refactor(measure_theory/lp_space): move most of the proof of mem_Lp.add to a new lemma in analysis/mean_inequalities (#5370)

Estimated changes