Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-13 12:42 8d7f0012

View on Github →

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.

Estimated changes