Theorem MeasureTheory.integral_fin_nat_prod_volume_eq_prod

Modification history

2025-06-01 16:11
Mathlib/MeasureTheory/Integral/Pi.lean
feat: generalize the Integral.Pi file from `volume` to other measures (#25329)
Added MeasureTheory.integral_fin_nat_prod_volume_eq_prodView on Github →