Theorem MeasurableEmbedding.prod_mk_right

Modification history

2025-03-08 05:09
Mathlib/MeasureTheory/MeasurableSpace/Prod.lean
chore(MeasureTheory,Probability): rename many lemmas (#22619) …
Deleted MeasurableEmbedding.prod_mk_rightView on Github →
2024-10-27 19:30
Mathlib/MeasureTheory/MeasurableSpace/Prod.lean
chore(MeasureTheory/Constructions/Prod/Basic: split (#18286) …
Modified MeasurableEmbedding.prod_mk_rightView on Github →
2024-01-18 15:15
Mathlib/MeasureTheory/Constructions/Prod/Basic.lean
feat(Probability): condKernel and condDistrib applied to singletons of non-zero measure (#9351) …
Added MeasurableEmbedding.prod_mk_rightView on Github →