chore: split Mathlib.Topology.Algebra.UniformGroup

Mathlib.lean

@@ -4669,7 +4669,8 @@ import Mathlib.Topology.Algebra.StarSubalgebra
 import Mathlib.Topology.Algebra.UniformConvergence
 import Mathlib.Topology.Algebra.UniformField
 import Mathlib.Topology.Algebra.UniformFilterBasis
-import Mathlib.Topology.Algebra.UniformGroup
+import Mathlib.Topology.Algebra.UniformGroup.Basic
+import Mathlib.Topology.Algebra.UniformGroup.Defs
 import Mathlib.Topology.Algebra.UniformMulAction
 import Mathlib.Topology.Algebra.UniformRing
 import Mathlib.Topology.Algebra.Valued.NormedValued

Mathlib/Analysis/Convex/TotallyBounded.lean

@@ -6,7 +6,7 @@ Authors: Christopher Hoskin
 
 import Mathlib.Topology.UniformSpace.Cauchy
 import Mathlib.Analysis.Convex.Hull
-import Mathlib.Topology.Algebra.UniformGroup
+import Mathlib.Topology.Algebra.UniformGroup.Basic
 import Mathlib.Topology.Algebra.Module.LocallyConvex
 
 /-!

Mathlib/Analysis/LocallyConvex/Bounded.lean

@@ -9,7 +9,7 @@ import Mathlib.Analysis.LocallyConvex.BalancedCoreHull
 import Mathlib.Analysis.Seminorm
 import Mathlib.LinearAlgebra.Basis.VectorSpace
 import Mathlib.Topology.Bornology.Basic
-import Mathlib.Topology.Algebra.UniformGroup
+import Mathlib.Topology.Algebra.UniformGroup.Basic
 import Mathlib.Topology.UniformSpace.Cauchy
 import Mathlib.Topology.Algebra.Module.Basic
 

Mathlib/Analysis/Normed/Group/Uniform.lean

@@ -3,7 +3,7 @@ Copyright (c) 2018 Patrick Massot. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Patrick Massot, Johannes Hölzl, Yaël Dillies
 -/
-import Mathlib.Topology.Algebra.UniformGroup
+import Mathlib.Topology.Algebra.UniformGroup.Basic
 import Mathlib.Topology.MetricSpace.Algebra
 import Mathlib.Topology.MetricSpace.IsometricSMul
 import Mathlib.Analysis.Normed.Group.Basic

Mathlib/Topology/Algebra/Equicontinuity.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anatole Dedecker
 -/
 import Mathlib.Topology.Algebra.UniformConvergence
+import Mathlib.Topology.UniformSpace.Equicontinuity
 
 /-!
 # Algebra-related equicontinuity criterions

Mathlib/Topology/Algebra/GroupCompletion.lean

@@ -3,7 +3,6 @@ Copyright (c) 2018 Patrick Massot. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Patrick Massot, Johannes Hölzl
 -/
-import Mathlib.Topology.Algebra.UniformGroup
 import Mathlib.Topology.Algebra.UniformMulAction
 import Mathlib.Topology.UniformSpace.Completion
 

Mathlib/Topology/Algebra/InfiniteSum/Group.lean

@@ -5,7 +5,8 @@ Authors: Johannes Hölzl
 -/
 import Mathlib.SetTheory.Cardinal.Finite
 import Mathlib.Topology.Algebra.InfiniteSum.Basic
-import Mathlib.Topology.Algebra.UniformGroup
+import Mathlib.Topology.UniformSpace.Cauchy
+import Mathlib.Topology.Algebra.UniformGroup.Defs
 
 /-!
 # Infinite sums and products in topological groups

Mathlib/Topology/Algebra/Module/Basic.lean

@@ -11,8 +11,9 @@ import Mathlib.LinearAlgebra.Pi
 import Mathlib.LinearAlgebra.Projection
 import Mathlib.Topology.Algebra.MulAction
 import Mathlib.Topology.Algebra.Ring.Basic
-import Mathlib.Topology.Algebra.UniformGroup
 import Mathlib.Topology.UniformSpace.UniformEmbedding
+import Mathlib.Topology.Algebra.Group.Quotient
+import Mathlib.Topology.Algebra.UniformGroup.Defs
 
 /-!
 # Theory of topological modules and continuous linear maps.

Mathlib/Topology/Algebra/UniformConvergence.lean

@@ -5,6 +5,7 @@ Authors: Anatole Dedecker
 -/
 import Mathlib.Topology.Algebra.UniformMulAction
 import Mathlib.Algebra.Module.Pi
+import Mathlib.Topology.UniformSpace.UniformConvergenceTopology
 
 /-!
 # Algebraic facts about the topology of uniform convergence

Mathlib/Topology/Algebra/UniformFilterBasis.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Patrick Massot
 -/
 import Mathlib.Topology.Algebra.FilterBasis
-import Mathlib.Topology.Algebra.UniformGroup
 
 /-!
 # Uniform properties of neighborhood bases in topological algebra