Theorem MeasureTheory.Measure.infinitePi_dirac

Modification history

2025-11-15 16:31
Mathlib/Probability/ProductMeasure.lean
feat: compute the PMF of a product measure (#31392) …
Added MeasureTheory.Measure.infinitePi_diracView on Github →