Commit 2020-11-20 12:39 498d4977
View on Github →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.
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.