Commit 2021-10-25 17:43 2026a5f7

feat(measure_theory/measure): better measure.restrict_singleton (#9936) With new restrict_singleton, simp can simplify ∫ x in {a}, f x ∂μ to (μ {a}).to_real • f a.