Commit 2023-12-10 14:38 390d5fb5

feat(MeasureTheory/Integral/Pi): dependent types, values in R or C (#8948) This is a generalisation of the lemmas in MeasureTheory.Integral.Pi to consider functions on products (i : ι) → E i, rather than just products of multiple copies of the same type. I also allowed complex-valued functions, and renamed some lemmas slightly (since the lemmas had finset in their names but were about fintypes, not finsets).