Commit 2019-11-29 16:54 817711d8

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