mathlib3

7c60702a - feat(measure_theory/integral): "integral_prod_mul" for complex coefficients (#18085)

feat(measure_theory/integral): "integral_prod_mul" for complex coefficients (#18085) This generalises some lemmas in the integration library, currently only stated for `ℝ`-valued functions, to allow complex-valued functions too. (Note that one can't generalise all the way to an arbitrary Banach algebra, there are problems when one side is integrable and the other isn't.)