[Merged by Bors] - feat(MeasureTheory): the integral of a vector-valued function against a vector measure is additive#30230

CoolRmal wants to merge 30 commits into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

CoolRmal:VectorMeasureIntegralCoolRmal/mathlib4:VectorMeasureIntegralCopy head branch name to clipboard