Theorem MeasureTheory.Measure.snd_map_prod_mk

Modification history

2025-03-08 05:09
Mathlib/MeasureTheory/Measure/Prod.lean
chore(MeasureTheory,Probability): rename many lemmas (#22619) …
Deleted MeasureTheory.Measure.snd_map_prod_mkView on Github →
2023-07-25 13:48
Mathlib/MeasureTheory/Constructions/Prod/Basic.lean
chore(Probability.Kernel): drop AEMeasurable assumptions (#6129)
Modified MeasureTheory.Measure.snd_map_prod_mkView on Github →
2023-06-20 13:55
Mathlib/MeasureTheory/Constructions/Prod/Basic.lean
chore: forward port leanprover-community/mathlib#19090 (#5291)
Added MeasureTheory.Measure.snd_map_prod_mkView on Github →