Theorem MeasureTheory.Measure.pi_pi_finset

Modification history

2026-03-13 23:21

Mathlib/MeasureTheory/Constructions/Pi.lean

feat(MeasureTheory/Constructions/Pi): add pi_pi_finset (#36288) …

Added MeasureTheory.Measure.pi_pi_finset View on Github →