Commit 2025-04-28 00:02 b8e91f67

feat(MeasureTheory): multiplication by a constant can be pulled out of an integral (#24397) This PR shows that ∫ x, f x * c ∂μ = (∫ x, f x ∂μ) * c and ∫ x, c * f x ∂μ = c * ∫ x, f x ∂μ when c is a constant, and where f takes values in a Banach algebra.