mathlib

b76d2b40 - feat(measure_theory/measurable_space): add `prod.measurable_singleton_class` (#16559)

feat(measure_theory/measurable_space): add `prod.measurable_singleton_class` (#16559) * golf `pi.measurable_singleton_class`, rename from `measurable_singleton_class.pi`; * add `prod.measurable_singleton_class`.