Theorem MeasureTheory.Measure.fst_map_prod_mk₀

Modification history

2023-07-25 13:48
Mathlib/MeasureTheory/Constructions/Prod/Basic.lean
chore(Probability.Kernel): drop AEMeasurable assumptions (#6129)
Modified MeasureTheory.Measure.fst_map_prod_mk₀View on Github →
2023-06-20 13:55
Mathlib/MeasureTheory/Constructions/Prod/Basic.lean
chore: forward port leanprover-community/mathlib#19090 (#5291)
Added MeasureTheory.Measure.fst_map_prod_mk₀View on Github →