Commit 2026-03-02 10:08 6bcaec3e
View on Github →feat(MeasureTheory): add lemma for sum_smul_dirac_singleton (#35835)
This PR adds a new lemma sum_smul_dirac_singleton that simplifies the evaluation of a sum of scaled Dirac measures on a singleton set.