Def MeasurableEquiv.piOptionEquivProd

Modification history

2024-06-19 09:36

Mathlib/MeasureTheory/MeasurableSpace/Basic.lean

chore: Split large file `MeasureTheory.MeasurableSpace.Basic` (#13937)

Modified MeasurableEquiv.piOptionEquivProd View on Github →

2024-04-26 11:43

Mathlib/MeasureTheory/MeasurableSpace/Basic.lean

feat: add MeasurableEquiv.piOptionEquivProd (#12395) …

Added MeasurableEquiv.piOptionEquivProd View on Github →