Commit 2023-06-20 13:55 76ed1a89

View on Github →

chore: forward port leanprover-community/mathlib#19090 (#5291)

Estimated changes

Modified Mathlib/MeasureTheory/Constructions/Prod/Basic.lean

added theorem MeasureTheory.Measure.fst_map_prod_mk

added theorem MeasureTheory.Measure.fst_map_prod_mk₀

added theorem MeasureTheory.Measure.snd_map_prod_mk

added theorem MeasureTheory.Measure.snd_map_prod_mk₀