Commit 2024-07-15 00:06 26110924

View on Github →

feat(MeasureTheory/Constructions/Pi): add measurePreserving_pi (#14185) See the Zulip thread

Estimated changes

Modified Mathlib/MeasureTheory/Constructions/Pi.lean

added theorem MeasureTheory.measurePreserving_pi

added theorem MeasureTheory.volume_preserving_pi