Theorem MeasureTheory.Measure.pi_pi

Modification history

2026-03-13 23:21
Mathlib/MeasureTheory/Constructions/Pi.lean
feat(MeasureTheory/Constructions/Pi): add pi_pi_finset (#36288) …
Modified MeasureTheory.Measure.pi_piView on Github →
2025-07-28 20:02
Mathlib/MeasureTheory/Constructions/Pi.lean
chore: remove useless assumption in measure instances (#27594)
Modified MeasureTheory.Measure.pi_piView on Github →
2023-06-01 03:52
Mathlib/MeasureTheory/Constructions/Pi.lean
feat: port MeasureTheory.Constructions.Pi (#4501)
Added MeasureTheory.Measure.pi_piView on Github →