mathlib3

347d2ed1 - feat(measure_theory/integrals): integration by parts for algebra-valued functions (#17778)

feat(measure_theory/integrals): integration by parts for algebra-valued functions (#17778) The code for integration by parts in the library presently assumes the functions are ℝ-valued. This generalises things to allow functions valued in a complete normed ℝ-algebra (not necessarily commutative); the motivating case is of course functions `ℝ → ℂ`.