Theorem MeasureTheory.Integrable.comp_snd_map_prod_id

Modification history

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_id View 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_id View on Github →