small changes

Author: CoolRmal

Mathlib/MeasureTheory/Integral/CompactlySupported.lean

@@ -4,12 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yongxi Lin, Thomas Zhu
 -/
 
-import Mathlib.GroupTheory.MonoidLocalization.Basic
 import Mathlib.MeasureTheory.Function.LocallyIntegrable
 import Mathlib.MeasureTheory.Integral.Bochner.Basic
 import Mathlib.Topology.ContinuousMap.CompactlySupported
 
-/-! This file contains definitions and lemmas related to integrals of compactly supported continuous
+/-!
+# Integrating compactly supported continuous functions
+This file contains definitions and lemmas related to integrals of compactly supported continuous
 functions.
 -/
 

Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/Basic.lean

@@ -27,6 +27,7 @@ literature.
 
 -/
 
+
 noncomputable section
 
 open scoped BoundedContinuousFunction NNReal ENNReal

Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/Real.lean

@@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yoh Tanimoto, Oliver Butterley
 -/
 import Mathlib.MeasureTheory.Integral.Bochner.Set
+import Mathlib.MeasureTheory.Integral.CompactlySupported
 import Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
 import Mathlib.Order.Interval.Set.Union
-import Mathlib.MeasureTheory.Integral.CompactlySupported
 
 /-!
 # Riesz–Markov–Kakutani representation theorem for real-linear functionals