refactor(MeasureTheory/Measure/Typeclasses/NoAtoms): add deprecation for NoAtoms (#40815)

ldiedering · ldiedering · commit b8ddb2552a4c · 2026-06-25T09:10:25.000Z
Add module deprecation for `MeasureTheory/Measure/Typeclasses/NoAtoms`.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -5595,6 +5595,7 @@ public import Mathlib.MeasureTheory.Measure.TightNormed
 public import Mathlib.MeasureTheory.Measure.Tilted
 public import Mathlib.MeasureTheory.Measure.Trim
 public import Mathlib.MeasureTheory.Measure.Typeclasses.Finite
+public import Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms
 public import Mathlib.MeasureTheory.Measure.Typeclasses.NullSingletonClass
 public import Mathlib.MeasureTheory.Measure.Typeclasses.Probability
 public import Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
diff --git a/Mathlib/MeasureTheory/Measure/Typeclasses/NoAtoms.lean b/Mathlib/MeasureTheory/Measure/Typeclasses/NoAtoms.lean
@@ -0,0 +1,9 @@
+module
+
+/-! # NoAtoms
+This file is deprecated. Please use `Mathlib.MeasureTheory.Measure.Typeclasses.NullSingletonClass`
+instead.
+-/
+
+deprecated_module "use Mathlib.MeasureTheory.Measure.Typeclasses.NullSingletonClass instead"
+  (since := "2026-06-19")
