Commit 2026-11-10 19:03 666ab9b6

feat(MeasureTheory): add IsAtom and NoAtoms (#45666) Define what an atom s of a measure μ is (IsAtom μ s), and define a nonatomic measure as a measure with no atoms (the new type class NoAtoms). As discussed here, an older definition of NoAtoms, deprecated and renamed to NullSingletonClass in #40809 and #40815, was weaker than the standard notion under that name. This PR also removes the deprecation warnings. Follow-up PRs are planned to add more API for the new definitions.