Commit 2026-03-02 10:08 dfa2fe75

feat(MeasureTheory): Add MeasurableSingletonClass version of Measure.map_dirac (#35784) Gives the new theorem the name Measure.map_dirac and rename the current Measure.map_dirac to Measure.map_dirac'. This follows a convention used elsewhere that for each Measure.dirac lemma with a MeasurableSingleton instance version and a version requiring some sort of measurability, the MeasurableSingleton version has the unprimed name, and the version requiring measurability has the primed name.