diff --git a/src/algebraic_geometry/locally_ringed_space.lean b/src/algebraic_geometry/locally_ringed_space.lean
index 99cc0267c1c1e..e5ea98be10c43 100644
--- a/src/algebraic_geometry/locally_ringed_space.lean
+++ b/src/algebraic_geometry/locally_ringed_space.lean
@@ -8,7 +8,7 @@ import algebraic_geometry.sheafed_space
 import algebra.category.CommRing.limits
 import algebra.category.CommRing.colimits
 import algebraic_geometry.stalks
-import ring_theory.ideal.basic
+import ring_theory.ideal.local_ring
 
 /-!
 # The category of locally ringed spaces
diff --git a/src/data/equiv/transfer_instance.lean b/src/data/equiv/transfer_instance.lean
index 18f6b5e8a4d1d..baab60ce59810 100644
--- a/src/data/equiv/transfer_instance.lean
+++ b/src/data/equiv/transfer_instance.lean
@@ -8,7 +8,7 @@ import algebra.field
 import algebra.module
 import algebra.algebra.basic
 import algebra.group.type_tags
-import ring_theory.ideal.basic
+import ring_theory.ideal.local_ring
 
 /-!
 # Transfer algebraic structures across `equiv`s
diff --git a/src/ring_theory/discrete_valuation_ring.lean b/src/ring_theory/discrete_valuation_ring.lean
index 07ad6a74f82b3..93e42acf3e474 100644
--- a/src/ring_theory/discrete_valuation_ring.lean
+++ b/src/ring_theory/discrete_valuation_ring.lean
@@ -6,6 +6,7 @@ Authors: Kevin Buzzard
 
 import ring_theory.principal_ideal_domain
 import order.conditionally_complete_lattice
+import ring_theory.ideal.local_ring
 import ring_theory.multiplicity
 import ring_theory.valuation.basic
 
diff --git a/src/ring_theory/ideal/basic.lean b/src/ring_theory/ideal/basic.lean
index be50543493ad8..94848393c7e87 100644
--- a/src/ring_theory/ideal/basic.lean
+++ b/src/ring_theory/ideal/basic.lean
@@ -775,213 +775,3 @@ begin
   rcases ideal.exists_le_maximal _ this with ⟨I, Imax, H⟩,
   use [I, Imax], apply H, apply ideal.subset_span, exact set.mem_singleton a
 end
-
-/-- A commutative ring is local if it has a unique maximal ideal. Note that
-  `local_ring` is a predicate. -/
-class local_ring (α : Type u) [comm_ring α] extends nontrivial α : Prop :=
-(is_local : ∀ (a : α), (is_unit a) ∨ (is_unit (1 - a)))
-
-namespace local_ring
-
-variables [comm_ring α] [local_ring α]
-
-lemma is_unit_or_is_unit_one_sub_self (a : α) :
-  (is_unit a) ∨ (is_unit (1 - a)) :=
-is_local a
-
-lemma is_unit_of_mem_nonunits_one_sub_self (a : α) (h : (1 - a) ∈ nonunits α) :
-  is_unit a :=
-or_iff_not_imp_right.1 (is_local a) h
-
-lemma is_unit_one_sub_self_of_mem_nonunits (a : α) (h : a ∈ nonunits α) :
-  is_unit (1 - a) :=
-or_iff_not_imp_left.1 (is_local a) h
-
-lemma nonunits_add {x y} (hx : x ∈ nonunits α) (hy : y ∈ nonunits α) :
-  x + y ∈ nonunits α :=
-begin
-  rintros ⟨u, hu⟩,
-  apply hy,
-  suffices : is_unit ((↑u⁻¹ : α) * y),
-  { rcases this with ⟨s, hs⟩,
-    use u * s,
-    convert congr_arg (λ z, (u : α) * z) hs,
-    rw ← mul_assoc, simp },
-  rw show (↑u⁻¹ * y) = (1 - ↑u⁻¹ * x),
-  { rw eq_sub_iff_add_eq,
-    replace hu := congr_arg (λ z, (↑u⁻¹ : α) * z) hu.symm,
-    simpa [mul_add, add_comm] using hu },
-  apply is_unit_one_sub_self_of_mem_nonunits,
-  exact mul_mem_nonunits_right hx
-end
-
-variable (α)
-
-/-- The ideal of elements that are not units. -/
-def maximal_ideal : ideal α :=
-{ carrier := nonunits α,
-  zero_mem' := zero_mem_nonunits.2 $ zero_ne_one,
-  add_mem' := λ x y hx hy, nonunits_add hx hy,
-  smul_mem' := λ a x, mul_mem_nonunits_right }
-
-instance maximal_ideal.is_maximal : (maximal_ideal α).is_maximal :=
-begin
-  rw ideal.is_maximal_iff,
-  split,
-  { intro h, apply h, exact is_unit_one },
-  { intros I x hI hx H,
-    erw not_not at hx,
-    rcases hx with ⟨u,rfl⟩,
-    simpa using I.mul_mem_left ↑u⁻¹ H }
-end
-
-lemma maximal_ideal_unique :
-  ∃! I : ideal α, I.is_maximal :=
-⟨maximal_ideal α, maximal_ideal.is_maximal α,
-  λ I hI, hI.eq_of_le (maximal_ideal.is_maximal α).1.1 $
-  λ x hx, hI.1.1 ∘ I.eq_top_of_is_unit_mem hx⟩
-
-variable {α}
-
-lemma eq_maximal_ideal {I : ideal α} (hI : I.is_maximal) : I = maximal_ideal α :=
-unique_of_exists_unique (maximal_ideal_unique α) hI $ maximal_ideal.is_maximal α
-
-lemma le_maximal_ideal {J : ideal α} (hJ : J ≠ ⊤) : J ≤ maximal_ideal α :=
-begin
-  rcases ideal.exists_le_maximal J hJ with ⟨M, hM1, hM2⟩,
-  rwa ←eq_maximal_ideal hM1
-end
-
-@[simp] lemma mem_maximal_ideal (x) :
-  x ∈ maximal_ideal α ↔ x ∈ nonunits α := iff.rfl
-
-end local_ring
-
-lemma local_of_nonunits_ideal [comm_ring α] (hnze : (0:α) ≠ 1)
-  (h : ∀ x y ∈ nonunits α, x + y ∈ nonunits α) : local_ring α :=
-{ exists_pair_ne := ⟨0, 1, hnze⟩,
-  is_local := λ x, or_iff_not_imp_left.mpr $ λ hx,
-  begin
-    by_contra H,
-    apply h _ _ hx H,
-    simp [-sub_eq_add_neg, add_sub_cancel'_right]
-  end }
-
-lemma local_of_unique_max_ideal [comm_ring α] (h : ∃! I : ideal α, I.is_maximal) :
-  local_ring α :=
-local_of_nonunits_ideal
-(let ⟨I, Imax, _⟩ := h in (λ (H : 0 = 1), Imax.1.1 $ I.eq_top_iff_one.2 $ H ▸ I.zero_mem))
-$ λ x y hx hy H,
-let ⟨I, Imax, Iuniq⟩ := h in
-let ⟨Ix, Ixmax, Hx⟩ := exists_max_ideal_of_mem_nonunits hx in
-let ⟨Iy, Iymax, Hy⟩ := exists_max_ideal_of_mem_nonunits hy in
-have xmemI : x ∈ I, from ((Iuniq Ix Ixmax) ▸ Hx),
-have ymemI : y ∈ I, from ((Iuniq Iy Iymax) ▸ Hy),
-Imax.1.1 $ I.eq_top_of_is_unit_mem (I.add_mem xmemI ymemI) H
-
-lemma local_of_unique_nonzero_prime (R : Type u) [comm_ring R]
-  (h : ∃! P : ideal R, P ≠ ⊥ ∧ ideal.is_prime P) : local_ring R :=
-local_of_unique_max_ideal begin
-  rcases h with ⟨P, ⟨hPnonzero, hPnot_top, _⟩, hPunique⟩,
-  refine ⟨P, ⟨⟨hPnot_top, _⟩⟩, λ M hM, hPunique _ ⟨_, ideal.is_maximal.is_prime hM⟩⟩,
-  { refine ideal.maximal_of_no_maximal (λ M hPM hM, ne_of_lt hPM _),
-    exact (hPunique _ ⟨ne_bot_of_gt hPM, ideal.is_maximal.is_prime hM⟩).symm },
-  { rintro rfl,
-    exact hPnot_top (hM.1.2 P (bot_lt_iff_ne_bot.2 hPnonzero)) },
-end
-
-lemma local_of_surjective {A B : Type*} [comm_ring A] [local_ring A] [comm_ring B] [nontrivial B]
-  (f : A →+* B) (hf : function.surjective f) :
-  local_ring B :=
-{ is_local :=
-  begin
-    intros b,
-    obtain ⟨a, rfl⟩ := hf b,
-    apply (local_ring.is_unit_or_is_unit_one_sub_self a).imp f.is_unit_map _,
-    rw [← f.map_one, ← f.map_sub],
-    apply f.is_unit_map,
-  end,
-  .. ‹nontrivial B› }
-
-/-- A local ring homomorphism is a homomorphism between local rings
-  such that the image of the maximal ideal of the source is contained within
-  the maximal ideal of the target. -/
-class is_local_ring_hom [semiring α] [semiring β] (f : α →+* β) : Prop :=
-(map_nonunit : ∀ a, is_unit (f a) → is_unit a)
-
-instance is_local_ring_hom_id (A : Type*) [semiring A] : is_local_ring_hom (ring_hom.id A) :=
-{ map_nonunit := λ a, id }
-
-@[simp] lemma is_unit_map_iff {A B : Type*} [semiring A] [semiring B] (f : A →+* B)
-  [is_local_ring_hom f] (a) :
-  is_unit (f a) ↔ is_unit a :=
-⟨is_local_ring_hom.map_nonunit a, f.is_unit_map⟩
-
-instance is_local_ring_hom_comp {A B C : Type*} [semiring A] [semiring B] [semiring C]
-  (g : B →+* C) (f : A →+* B) [is_local_ring_hom g] [is_local_ring_hom f] :
-  is_local_ring_hom (g.comp f) :=
-{ map_nonunit := λ a, is_local_ring_hom.map_nonunit a ∘ is_local_ring_hom.map_nonunit (f a) }
-
-@[simp] lemma is_unit_of_map_unit [semiring α] [semiring β] (f : α →+* β) [is_local_ring_hom f]
-  (a) (h : is_unit (f a)) : is_unit a :=
-is_local_ring_hom.map_nonunit a h
-
-theorem of_irreducible_map [semiring α] [semiring β] (f : α →+* β) [h : is_local_ring_hom f] {x : α}
-  (hfx : irreducible (f x)) : irreducible x :=
-⟨λ h, hfx.not_unit $ is_unit.map f.to_monoid_hom h, λ p q hx, let ⟨H⟩ := h in
-or.imp (H p) (H q) $ hfx.is_unit_or_is_unit $ f.map_mul p q ▸ congr_arg f hx⟩
-
-section
-open local_ring
-variables [comm_ring α] [local_ring α] [comm_ring β] [local_ring β]
-variables (f : α →+* β) [is_local_ring_hom f]
-
-lemma map_nonunit (a) (h : a ∈ maximal_ideal α) : f a ∈ maximal_ideal β :=
-λ H, h $ is_unit_of_map_unit f a H
-
-end
-
-namespace local_ring
-variables [comm_ring α] [local_ring α] [comm_ring β] [local_ring β]
-
-variable (α)
-/-- The residue field of a local ring is the quotient of the ring by its maximal ideal. -/
-def residue_field := (maximal_ideal α).quotient
-
-noncomputable instance residue_field.field : field (residue_field α) :=
-ideal.quotient.field (maximal_ideal α)
-
-noncomputable instance : inhabited (residue_field α) := ⟨37⟩
-
-/-- The quotient map from a local ring to its residue field. -/
-def residue : α →+* (residue_field α) :=
-ideal.quotient.mk _
-
-namespace residue_field
-
-variables {α β}
-/-- The map on residue fields induced by a local homomorphism between local rings -/
-noncomputable def map (f : α →+* β) [is_local_ring_hom f] :
-  residue_field α →+* residue_field β :=
-ideal.quotient.lift (maximal_ideal α) ((ideal.quotient.mk _).comp f) $
-λ a ha,
-begin
-  erw ideal.quotient.eq_zero_iff_mem,
-  exact map_nonunit f a ha
-end
-
-end residue_field
-
-end local_ring
-
-namespace field
-variables [field α]
-
-@[priority 100] -- see Note [lower instance priority]
-instance : local_ring α :=
-{ is_local := λ a,
-  if h : a = 0
-  then or.inr (by rw [h, sub_zero]; exact is_unit_one)
-  else or.inl $ is_unit.mk0 a h }
-
-end field
diff --git a/src/ring_theory/ideal/local_ring.lean b/src/ring_theory/ideal/local_ring.lean
new file mode 100644
index 0000000000000..f781ab6a4877c
--- /dev/null
+++ b/src/ring_theory/ideal/local_ring.lean
@@ -0,0 +1,243 @@
+/-
+Copyright (c) 2018 Kenny Lau. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kenny Lau, Chris Hughes, Mario Carneiro
+-/
+import algebra.category.CommRing.basic
+import ring_theory.ideal.basic
+
+/-!
+
+# Local rings
+
+Define local rings as commutative rings having a unique maximal ideal.
+
+## Main definitions
+
+* `local_ring`: A predicate on commutative rings, stating that every element `a` is either a unit
+  or `1 - a` is a unit. This is shown to be equivalent to the condition that there exists a unique
+  maximal ideal.
+* `local_ring.maximal_ideal`: The unique maximal ideal for a local rings. Its carrier set is the set
+  of non units.
+* `is_local_ring_hom`: A predicate on semiring homomorphisms, requiring that it maps nonunits
+  to nonunits. For local rings, this means that the image of the unique maximal ideal is again
+  contained in the unique maximal ideal.
+* `local_ring.residue_field`: The quotient of a local ring by its maximal ideal.
+
+-/
+
+universes u v w
+
+/-- A commutative ring is local if it has a unique maximal ideal. Note that
+  `local_ring` is a predicate. -/
+class local_ring (R : Type u) [comm_ring R] extends nontrivial R : Prop :=
+(is_local : ∀ (a : R), (is_unit a) ∨ (is_unit (1 - a)))
+
+namespace local_ring
+
+variables {R : Type u} [comm_ring R] [local_ring R]
+
+lemma is_unit_or_is_unit_one_sub_self (a : R) :
+  (is_unit a) ∨ (is_unit (1 - a)) :=
+is_local a
+
+lemma is_unit_of_mem_nonunits_one_sub_self (a : R) (h : (1 - a) ∈ nonunits R) :
+  is_unit a :=
+or_iff_not_imp_right.1 (is_local a) h
+
+lemma is_unit_one_sub_self_of_mem_nonunits (a : R) (h : a ∈ nonunits R) :
+  is_unit (1 - a) :=
+or_iff_not_imp_left.1 (is_local a) h
+
+lemma nonunits_add {x y} (hx : x ∈ nonunits R) (hy : y ∈ nonunits R) :
+  x + y ∈ nonunits R :=
+begin
+  rintros ⟨u, hu⟩,
+  apply hy,
+  suffices : is_unit ((↑u⁻¹ : R) * y),
+  { rcases this with ⟨s, hs⟩,
+    use u * s,
+    convert congr_arg (λ z, (u : R) * z) hs,
+    rw ← mul_assoc, simp },
+  rw show (↑u⁻¹ * y) = (1 - ↑u⁻¹ * x),
+  { rw eq_sub_iff_add_eq,
+    replace hu := congr_arg (λ z, (↑u⁻¹ : R) * z) hu.symm,
+    simpa [mul_add, add_comm] using hu },
+  apply is_unit_one_sub_self_of_mem_nonunits,
+  exact mul_mem_nonunits_right hx
+end
+
+variable (R)
+
+/-- The ideal of elements that are not units. -/
+def maximal_ideal : ideal R :=
+{ carrier := nonunits R,
+  zero_mem' := zero_mem_nonunits.2 $ zero_ne_one,
+  add_mem' := λ x y hx hy, nonunits_add hx hy,
+  smul_mem' := λ a x, mul_mem_nonunits_right }
+
+instance maximal_ideal.is_maximal : (maximal_ideal R).is_maximal :=
+begin
+  rw ideal.is_maximal_iff,
+  split,
+  { intro h, apply h, exact is_unit_one },
+  { intros I x hI hx H,
+    erw not_not at hx,
+    rcases hx with ⟨u,rfl⟩,
+    simpa using I.mul_mem_left ↑u⁻¹ H }
+end
+
+lemma maximal_ideal_unique :
+  ∃! I : ideal R, I.is_maximal :=
+⟨maximal_ideal R, maximal_ideal.is_maximal R,
+  λ I hI, hI.eq_of_le (maximal_ideal.is_maximal R).1.1 $
+  λ x hx, hI.1.1 ∘ I.eq_top_of_is_unit_mem hx⟩
+
+variable {R}
+
+lemma eq_maximal_ideal {I : ideal R} (hI : I.is_maximal) : I = maximal_ideal R :=
+unique_of_exists_unique (maximal_ideal_unique R) hI $ maximal_ideal.is_maximal R
+
+lemma le_maximal_ideal {J : ideal R} (hJ : J ≠ ⊤) : J ≤ maximal_ideal R :=
+begin
+  rcases ideal.exists_le_maximal J hJ with ⟨M, hM1, hM2⟩,
+  rwa ←eq_maximal_ideal hM1
+end
+
+@[simp] lemma mem_maximal_ideal (x) :
+  x ∈ maximal_ideal R ↔ x ∈ nonunits R := iff.rfl
+
+end local_ring
+
+variables {R : Type u} {S : Type v} {T : Type w}
+
+lemma local_of_nonunits_ideal [comm_ring R] (hnze : (0:R) ≠ 1)
+  (h : ∀ x y ∈ nonunits R, x + y ∈ nonunits R) : local_ring R :=
+{ exists_pair_ne := ⟨0, 1, hnze⟩,
+  is_local := λ x, or_iff_not_imp_left.mpr $ λ hx,
+  begin
+    by_contra H,
+    apply h _ _ hx H,
+    simp [-sub_eq_add_neg, add_sub_cancel'_right]
+  end }
+
+lemma local_of_unique_max_ideal [comm_ring R] (h : ∃! I : ideal R, I.is_maximal) :
+  local_ring R :=
+local_of_nonunits_ideal
+(let ⟨I, Imax, _⟩ := h in (λ (H : 0 = 1), Imax.1.1 $ I.eq_top_iff_one.2 $ H ▸ I.zero_mem))
+$ λ x y hx hy H,
+let ⟨I, Imax, Iuniq⟩ := h in
+let ⟨Ix, Ixmax, Hx⟩ := exists_max_ideal_of_mem_nonunits hx in
+let ⟨Iy, Iymax, Hy⟩ := exists_max_ideal_of_mem_nonunits hy in
+have xmemI : x ∈ I, from ((Iuniq Ix Ixmax) ▸ Hx),
+have ymemI : y ∈ I, from ((Iuniq Iy Iymax) ▸ Hy),
+Imax.1.1 $ I.eq_top_of_is_unit_mem (I.add_mem xmemI ymemI) H
+
+lemma local_of_unique_nonzero_prime (R : Type u) [comm_ring R]
+  (h : ∃! P : ideal R, P ≠ ⊥ ∧ ideal.is_prime P) : local_ring R :=
+local_of_unique_max_ideal begin
+  rcases h with ⟨P, ⟨hPnonzero, hPnot_top, _⟩, hPunique⟩,
+  refine ⟨P, ⟨⟨hPnot_top, _⟩⟩, λ M hM, hPunique _ ⟨_, ideal.is_maximal.is_prime hM⟩⟩,
+  { refine ideal.maximal_of_no_maximal (λ M hPM hM, ne_of_lt hPM _),
+    exact (hPunique _ ⟨ne_bot_of_gt hPM, ideal.is_maximal.is_prime hM⟩).symm },
+  { rintro rfl,
+    exact hPnot_top (hM.1.2 P (bot_lt_iff_ne_bot.2 hPnonzero)) },
+end
+
+lemma local_of_surjective [comm_ring R] [local_ring R] [comm_ring S] [nontrivial S]
+  (f : R →+* S) (hf : function.surjective f) :
+  local_ring S :=
+{ is_local :=
+  begin
+    intros b,
+    obtain ⟨a, rfl⟩ := hf b,
+    apply (local_ring.is_unit_or_is_unit_one_sub_self a).imp f.is_unit_map _,
+    rw [← f.map_one, ← f.map_sub],
+    apply f.is_unit_map,
+  end,
+  .. ‹nontrivial S› }
+
+/-- A local ring homomorphism is a homomorphism between local rings
+  such that the image of the maximal ideal of the source is contained within
+  the maximal ideal of the target. -/
+class is_local_ring_hom [semiring R] [semiring S] (f : R →+* S) : Prop :=
+(map_nonunit : ∀ a, is_unit (f a) → is_unit a)
+
+instance is_local_ring_hom_id (R : Type*) [semiring R] : is_local_ring_hom (ring_hom.id R) :=
+{ map_nonunit := λ a, id }
+
+@[simp] lemma is_unit_map_iff [semiring R] [semiring S] (f : R →+* S)
+  [is_local_ring_hom f] (a) :
+  is_unit (f a) ↔ is_unit a :=
+⟨is_local_ring_hom.map_nonunit a, f.is_unit_map⟩
+
+instance is_local_ring_hom_comp [semiring R] [semiring S] [semiring T]
+  (g : S →+* T) (f : R →+* S) [is_local_ring_hom g] [is_local_ring_hom f] :
+  is_local_ring_hom (g.comp f) :=
+{ map_nonunit := λ a, is_local_ring_hom.map_nonunit a ∘ is_local_ring_hom.map_nonunit (f a) }
+
+@[simp] lemma is_unit_of_map_unit [semiring R] [semiring S] (f : R →+* S) [is_local_ring_hom f]
+  (a) (h : is_unit (f a)) : is_unit a :=
+is_local_ring_hom.map_nonunit a h
+
+theorem of_irreducible_map [semiring R] [semiring S] (f : R →+* S) [h : is_local_ring_hom f] {x : R}
+  (hfx : irreducible (f x)) : irreducible x :=
+⟨λ h, hfx.not_unit $ is_unit.map f.to_monoid_hom h, λ p q hx, let ⟨H⟩ := h in
+or.imp (H p) (H q) $ hfx.is_unit_or_is_unit $ f.map_mul p q ▸ congr_arg f hx⟩
+
+section
+open local_ring
+variables [comm_ring R] [local_ring R] [comm_ring S] [local_ring S]
+variables (f : R →+* S) [is_local_ring_hom f]
+
+lemma map_nonunit (a : R) (h : a ∈ maximal_ideal R) : f a ∈ maximal_ideal S :=
+λ H, h $ is_unit_of_map_unit f a H
+
+end
+
+namespace local_ring
+variables [comm_ring R] [local_ring R] [comm_ring S] [local_ring S]
+
+variable (R)
+/-- The residue field of a local ring is the quotient of the ring by its maximal ideal. -/
+def residue_field := (maximal_ideal R).quotient
+
+noncomputable instance residue_field.field : field (residue_field R) :=
+ideal.quotient.field (maximal_ideal R)
+
+noncomputable instance : inhabited (residue_field R) := ⟨37⟩
+
+/-- The quotient map from a local ring to its residue field. -/
+def residue : R →+* (residue_field R) :=
+ideal.quotient.mk _
+
+namespace residue_field
+
+variables {R S}
+/-- The map on residue fields induced by a local homomorphism between local rings -/
+noncomputable def map (f : R →+* S) [is_local_ring_hom f] :
+  residue_field R →+* residue_field S :=
+ideal.quotient.lift (maximal_ideal R) ((ideal.quotient.mk _).comp f) $
+λ a ha,
+begin
+  erw ideal.quotient.eq_zero_iff_mem,
+  exact map_nonunit f a ha
+end
+
+end residue_field
+
+end local_ring
+
+namespace field
+variables [field R]
+
+open_locale classical
+
+@[priority 100] -- see Note [lower instance priority]
+instance : local_ring R :=
+{ is_local := λ a,
+  if h : a = 0
+  then or.inr (by rw [h, sub_zero]; exact is_unit_one)
+  else or.inl $ is_unit.mk0 a h }
+
+end field
diff --git a/src/ring_theory/localization.lean b/src/ring_theory/localization.lean
index 2d2c9116190cc..1bc063913fa76 100644
--- a/src/ring_theory/localization.lean
+++ b/src/ring_theory/localization.lean
@@ -7,6 +7,7 @@ Authors: Kenny Lau, Mario Carneiro, Johan Commelin, Amelia Livingston
 import data.equiv.ring
 import group_theory.monoid_localization
 import ring_theory.ideal.operations
+import ring_theory.ideal.local_ring
 import ring_theory.algebraic
 import ring_theory.integral_closure
 import ring_theory.non_zero_divisors
diff --git a/src/ring_theory/power_series/basic.lean b/src/ring_theory/power_series/basic.lean
index 4e35fbb429c5d..13150f47cb64e 100644
--- a/src/ring_theory/power_series/basic.lean
+++ b/src/ring_theory/power_series/basic.lean
@@ -5,6 +5,7 @@ Authors: Johan Commelin, Kenny Lau
 -/
 import data.mv_polynomial
 import linear_algebra.std_basis
+import ring_theory.ideal.local_ring
 import ring_theory.ideal.operations
 import ring_theory.multiplicity
 import ring_theory.algebra_tower