Theorem MeasureTheory.Integrable.fintype_prod_dep
Modification history
2025-06-01 16:11
Mathlib/MeasureTheory/Integral/Pi.lean
feat: generalize the Integral.Pi file from `volume` to other measures (#25329)
Modified MeasureTheory.Integrable.fintype_prod_depView on Github →