Theorem MeasureTheory.Integrable.comp_snd_map_prod_id

Modification history

2026-08-26 08:21
Mathlib/Probability/Kernel/Condexp.lean
refactor: change the default value of `Measure.map` to a Dirac mass (#42322) …
Modified MeasureTheory.Integrable.comp_snd_map_prod_idView on Github →
2025-12-03 12:39
Mathlib/Probability/Kernel/Condexp.lean
feat: drop unnecessary assumption in `MeasureTheory.Integrable.comp_snd_map_prod_id` (#32392)
Modified MeasureTheory.Integrable.comp_snd_map_prod_idView on Github →
2023-06-21 05:19
Mathlib/Probability/Kernel/Condexp.lean
feat: port Probability.Kernel.Condexp (#5324)
Added MeasureTheory.Integrable.comp_snd_map_prod_idView on Github →