mathlib3

498d4977 - feat(measure_theory/lp_space): prove that neg and add are in Lp (#5014)

feat(measure_theory/lp_space): prove that neg and add are in Lp (#5014) For f and g in Lp, (-f) and (f+g) are also in Lp. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>