Commit 2024-10-19 06:53 90c6be64

View on Github →

feat(MeasureTheory): μ.comap Prod.swap = μ.map Prod.swap (#17918) From PFR

Estimated changes

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

added theorem MeasureTheory.Measure.comap_swap