Commit 2022-12-05 09:33 347d2ed1
View on Github →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 ℝ → ℂ
.