Commit 2024-10-13 09:56 7306a036
View on Github →feat(MeasureTheory): two lemmas about Measure.bind (#17630)
Add two simp lemmas bind_const and bind_dirac_eq_map.
Swap the names of bind_dirac and dirac_bind for coherence with the other names in the file.