mathlib3

817711d8 - feat(measure_theory/bochner_integration): linearity of the Bochner Integral (#1745)

feat(measure_theory/bochner_integration): linearity of the Bochner Integral (#1745) * Linearity of the Bochner Integral * prove integral_neg and integral_smul with less assumptions; make integral irreducible * remove simp tag * create simp set for integral * Add simp_attr.integral to nolint * Make it possible to unfold the definition of `integral` and other things. * Update nolints.txt * Make it possible to unfold l1.integral * Update bochner_integration.lean * Update bochner_integration.lean