Theorem MeasureTheory.Measure.pi_singleton

Modification history

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