Theorem MeasureTheory.Measure.pi_eq

Modification history

2025-07-28 20:02

Mathlib/MeasureTheory/Constructions/Pi.lean

chore: remove useless assumption in measure instances (#27594)

Modified MeasureTheory.Measure.pi_eq View on Github →

2023-06-01 03:52

Mathlib/MeasureTheory/Constructions/Pi.lean

feat: port MeasureTheory.Constructions.Pi (#4501)

Added MeasureTheory.Measure.pi_eq View on Github →