mathlib

4ac69b29 - feat(probability/probability_mass_function): basic lawful monad lemmas for `pmf`. (#18469)

feat(probability/probability_mass_function): basic lawful monad lemmas for `pmf`. (#18469) This file adds basic lemmas for monadic operations on `pmf`, mirroring the lemmas for `is_lawful_monad`.