mathlib

9824a558 - feat(measure_theory/measurable_space): pi has measurable singletons (#16542)

feat(measure_theory/measurable_space): pi has measurable singletons (#16542) This generalises a result used for the birthday problem. Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com>