Theorem MeasureTheory.setLIntegral_prod

Modification history

2025-03-11 16:25
Mathlib/MeasureTheory/Measure/Prod.lean
feat(MeasureTheory): `setLIntegral_prod_symm` (#22735) …
Modified MeasureTheory.setLIntegral_prodView on Github →
2025-02-11 12:41
Mathlib/MeasureTheory/Measure/Prod.lean
feat(MeasureTheory/Prod): add a version of `lintegral_prod` for `setLIntegral`. (#21598) …
Added MeasureTheory.setLIntegral_prodView on Github →