mathlib3

154a0242 - feat(measure_theory/lp_space): add lemmas about the monotonicity of the Lp seminorm (#5395)

feat(measure_theory/lp_space): add lemmas about the monotonicity of the Lp seminorm (#5395) Also add a lemma mem_Lp.const_smul for a normed space. Co-authored-by: Rémy Degenne <remydegenne@gmail.com>