Commit 2025-03-06 15:53 3800f46f

chore: drop the explicit MeasurableSpace argument in iIndepFun (#22644) We make it a typeclass argument instead. Experience in PFR has shown that one essentially always uses the canonical measurable structure there, and that having an explicit argument is mostly redundant. Still, we keep a named typeclass argument, so that one can easily instantiate it explicitly if/when needed (but this is nowhere needed in current mathlib!)