mathlib

8d7f0012 - feat(measure_theory/pmf): lawful monad instance for probability mass function monad (#15066)

feat(measure_theory/pmf): lawful monad instance for probability mass function monad (#15066) Provide `is_lawful_functor` and `is_lawful_monad` instances for `pmf`. Also switch the `seq` and `map` operations to the ones coming from the `monad` instance. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>