mathlib

a196f9be - chore(measure_theory/probability_mass_function): Move pmf monad operations into a seperate file (#11579)

chore(measure_theory/probability_mass_function): Move pmf monad operations into a seperate file (#11579) This PR moves the `pure`, `bind`, and `bind_on_support` operations on `pmf` into a new `probability_mass_function/monad.lean` file.