Commit 2025-12-03 12:39 6b2aef46

View on Github →

feat: drop unnecessary assumption in MeasureTheory.Integrable.comp_snd_map_prod_id (#32392)

Estimated changes

Modified Mathlib/Probability/Kernel/Condexp.lean

modified theorem MeasureTheory.Integrable.comp_snd_map_prod_id