chore(AdicCompletion): move to RingTheory and make folder (#12511)

Move `AdicCompletion` from `LinearAlgebra` into its own folder in `RingTheory` as it seems to fit better there.
leanprover-community · Apr 29, 2024 · 283ea7e · 283ea7e
1 parent 9cbb31e
commit 283ea7e
Show file tree

Hide file tree

Showing 4 changed files with 3 additions and 3 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -2549,7 +2549,6 @@ import Mathlib.Lean.Meta.Simp
 import Mathlib.Lean.Name
 import Mathlib.Lean.PrettyPrinter.Delaborator
 import Mathlib.Lean.Thunk
-import Mathlib.LinearAlgebra.AdicCompletion
 import Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
 import Mathlib.LinearAlgebra.AffineSpace.AffineMap
 import Mathlib.LinearAlgebra.AffineSpace.AffineSubspace
@@ -3336,6 +3335,7 @@ import Mathlib.RepresentationTheory.GroupCohomology.Resolution
 import Mathlib.RepresentationTheory.Invariants
 import Mathlib.RepresentationTheory.Maschke
 import Mathlib.RepresentationTheory.Rep
+import Mathlib.RingTheory.AdicCompletion.Basic
 import Mathlib.RingTheory.Adjoin.Basic
 import Mathlib.RingTheory.Adjoin.FG
 import Mathlib.RingTheory.Adjoin.Field

diff --git a/Mathlib/LinearAlgebra/AdicCompletion.lean → Mathlib/RingTheory/AdicCompletion/Basic.lean b/Mathlib/LinearAlgebra/AdicCompletion.lean → Mathlib/RingTheory/AdicCompletion/Basic.lean
diff --git a/Mathlib/RingTheory/DiscreteValuationRing/Basic.lean b/Mathlib/RingTheory/DiscreteValuationRing/Basic.lean
@@ -6,7 +6,7 @@ Authors: Kevin Buzzard
 import Mathlib.RingTheory.PrincipalIdealDomain
 import Mathlib.RingTheory.Ideal.LocalRing
 import Mathlib.RingTheory.Valuation.PrimeMultiplicity
-import Mathlib.LinearAlgebra.AdicCompletion
+import Mathlib.RingTheory.AdicCompletion.Basic
 
 #align_import ring_theory.discrete_valuation_ring.basic from "leanprover-community/mathlib"@"c163ec99dfc664628ca15d215fce0a5b9c265b68"
 

diff --git a/Mathlib/RingTheory/Henselian.lean b/Mathlib/RingTheory/Henselian.lean
@@ -5,7 +5,7 @@ Authors: Johan Commelin
 -/
 import Mathlib.Algebra.Polynomial.Taylor
 import Mathlib.RingTheory.Ideal.LocalRing
-import Mathlib.LinearAlgebra.AdicCompletion
+import Mathlib.RingTheory.AdicCompletion.Basic
 
 #align_import ring_theory.henselian from "leanprover-community/mathlib"@"d1accf4f9cddb3666c6e8e4da0ac2d19c4ed73f0"