Commit 2022-12-05 09:33 347d2ed1

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 ℝ → ℂ.