diff --git a/src/algebra/gcd_monoid/integrally_closed.lean b/src/algebra/gcd_monoid/integrally_closed.lean
index 341d93937c36b..47ff732f99523 100644
--- a/src/algebra/gcd_monoid/integrally_closed.lean
+++ b/src/algebra/gcd_monoid/integrally_closed.lean
@@ -5,7 +5,7 @@ Authors: Andrew Yang
 -/
 import algebra.gcd_monoid.basic
 import ring_theory.integrally_closed
-import ring_theory.polynomial.eisenstein
+import ring_theory.polynomial.eisenstein.basic
 
 /-!
 
diff --git a/src/field_theory/minpoly/default.lean b/src/field_theory/minpoly/default.lean
index aa4d2da646584..e7bc53a8783e6 100644
--- a/src/field_theory/minpoly/default.lean
+++ b/src/field_theory/minpoly/default.lean
@@ -1,3 +1,3 @@
 import field_theory.minpoly.basic
 import field_theory.minpoly.field
-import field_theory.minpoly.gcd_monoid
+import field_theory.minpoly.is_integrally_closed
diff --git a/src/field_theory/minpoly/gcd_monoid.lean b/src/field_theory/minpoly/is_integrally_closed.lean
similarity index 53%
rename from src/field_theory/minpoly/gcd_monoid.lean
rename to src/field_theory/minpoly/is_integrally_closed.lean
index 5f14cb650f03c..37c45db1fdf8e 100644
--- a/src/field_theory/minpoly/gcd_monoid.lean
+++ b/src/field_theory/minpoly/is_integrally_closed.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2019 Riccardo Brasca. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Riccardo Brasca
+Authors: Riccardo Brasca, Paul Lezeau, Junyan Xu
 -/
 import data.polynomial.field_division
 import ring_theory.adjoin_root
@@ -15,23 +15,16 @@ This file specializes the theory of minpoly to the case of an algebra over a GCD
 
 ## Main results
 
- * `gcd_domain_eq_field_fractions`: For GCD domains, the minimal polynomial over the ring is the
-    same as the minimal polynomial over the fraction field.
-
- * `gcd_domain_dvd` : For GCD domains, the minimal polynomial divides any primitive polynomial
-    that has the integral element as root.
-
- * `gcd_domain_unique` : The minimal polynomial of an element `x` is uniquely characterized by
-    its defining property: if there is another monic polynomial of minimal degree that has `x` as a
-    root, then this polynomial is equal to the minimal polynomial of `x`.
-
  * `is_integrally_closed_eq_field_fractions`: For integrally closed domains, the minimal polynomial
     over the ring is the same as the minimal polynomial over the fraction field.
 
-## Todo
+ * `is_integrally_closed_dvd` : For integrally closed domains, the minimal polynomial divides any
+    primitive polynomial that has the integral element as root.
+
+ * `is_integrally_closed_unique` : The minimal polynomial of an element `x` is uniquely
+    characterized by its defining property: if there is another monic polynomial of minimal degree
+    that has `x` as a root, then this polynomial is equal to the minimal polynomial of `x`.
 
- * Remove all results that are now special cases (e.g. we no longer need `gcd_monoid_dvd` since we
-    have `is_integrally_closed_dvd`).
 -/
 
 open_locale classical polynomial
@@ -41,43 +34,11 @@ namespace minpoly
 
 variables {R S : Type*} [comm_ring R] [comm_ring S] [is_domain R] [algebra R S]
 
-
 section
 
 variables (K L : Type*) [field K] [algebra R K] [is_fraction_ring R K] [field L] [algebra R L]
  [algebra S L] [algebra K L] [is_scalar_tower R K L] [is_scalar_tower R S L]
 
-section gcd_domain
-
-variable [normalized_gcd_monoid R]
-
-/-- For GCD domains, the minimal polynomial over the ring is the same as the minimal polynomial
-over the fraction field. See `minpoly.gcd_domain_eq_field_fractions'` if `S` is already a
-`K`-algebra. -/
-lemma gcd_domain_eq_field_fractions [is_domain S] {s : S} (hs : is_integral R s) :
-  minpoly K (algebra_map S L s) = (minpoly R s).map (algebra_map R K) :=
-begin
-  refine (eq_of_irreducible_of_monic _ _ _).symm,
-  { exact (polynomial.is_primitive.irreducible_iff_irreducible_map_fraction_map
-      (polynomial.monic.is_primitive (monic hs))).1 (irreducible hs) },
-   { rw [aeval_map_algebra_map, aeval_algebra_map_apply, aeval, map_zero] },
-  { exact (monic hs).map _ }
-end
-
-/-- For GCD domains, the minimal polynomial over the ring is the same as the minimal polynomial
-over the fraction field. Compared to `minpoly.gcd_domain_eq_field_fractions`, this version is useful
-if the element is in a ring that is already a `K`-algebra. -/
-lemma gcd_domain_eq_field_fractions' [is_domain S] [algebra K S] [is_scalar_tower R K S]
-  {s : S} (hs : is_integral R s) : minpoly K s = (minpoly R s).map (algebra_map R K) :=
-begin
-  let L := fraction_ring S,
-  rw [← gcd_domain_eq_field_fractions K L hs],
-  refine minpoly.eq_of_algebra_map_eq (is_fraction_ring.injective S L)
-    (is_integral_of_is_scalar_tower hs) rfl
-end
-
-end gcd_domain
-
 variables [is_integrally_closed R]
 
 /-- For integrally closed domains, the minimal polynomial over the ring is the same as the minimal
@@ -105,76 +66,19 @@ begin
     (is_integral_of_is_scalar_tower hs) rfl
 end
 
-/-- For GCD domains, the minimal polynomial over the ring is the same as the minimal polynomial
-over the fraction field. Compared to `minpoly.is_integrally_closed_eq_field_fractions`, this
-version is useful if the element is in a ring that is not a domain -/
-theorem is_integrally_closed_eq_field_fractions'' [no_zero_smul_divisors S L] {s : S}
-  (hs : is_integral R s) : minpoly K (algebra_map S L s) = map (algebra_map R K) (minpoly R s) :=
-begin
-  --the idea of the proof is the following: since the minpoly of `a` over `Frac(R)` divides the
-  --minpoly of `a` over `R`, it is itself in `R`. Hence its degree is greater or equal to that of
-  --the minpoly of `a` over `R`. But the minpoly of `a` over `Frac(R)` divides the minpoly of a
-  --over `R` in `R[X]` so we are done.
-
-  --a few "trivial" preliminary results to set up the proof
-  have lem0 : minpoly K (algebra_map S L s) ∣ (map (algebra_map R K) (minpoly R s)),
-  { exact dvd_map_of_is_scalar_tower' R K L s },
-
-  have lem1 : is_integral K (algebra_map S L s),
-  { refine is_integral_map_of_comp_eq_of_is_integral (algebra_map R K) _ _ hs,
-    rw [← is_scalar_tower.algebra_map_eq, ← is_scalar_tower.algebra_map_eq] },
-
-  obtain ⟨g, hg⟩ := is_integrally_closed.eq_map_mul_C_of_dvd K (minpoly.monic hs) lem0,
-  rw [(minpoly.monic lem1).leading_coeff, C_1, mul_one] at hg,
-    have lem2 : polynomial.aeval s g = 0,
-  { have := minpoly.aeval K (algebra_map S L s),
-    rw [← hg, ← map_aeval_eq_aeval_map, ← map_zero (algebra_map S L)] at this,
-    { exact no_zero_smul_divisors.algebra_map_injective S L this },
-    { rw [← is_scalar_tower.algebra_map_eq, ← is_scalar_tower.algebra_map_eq] } },
-
-  have lem3 : g.monic,
-  { simpa only [function.injective.monic_map_iff (is_fraction_ring.injective R K), hg]
-      using minpoly.monic lem1 },
-
-  rw [← hg],
-  refine congr_arg _ (eq.symm (polynomial.eq_of_monic_of_dvd_of_nat_degree_le lem3
-    (minpoly.monic hs) _ _)),
-  { rwa [← map_dvd_map _ (is_fraction_ring.injective R K) lem3, hg] },
-  { exact nat_degree_le_nat_degree (minpoly.min R s lem3 lem2) },
-end
-
 end
 
 variables [is_domain S] [no_zero_smul_divisors R S]
 
-lemma gcd_domain_dvd [normalized_gcd_monoid R] {s : S} (hs : is_integral R s) {P : R[X]}
-  (hP : P ≠ 0) (hroot : polynomial.aeval s P = 0) : minpoly R s ∣ P :=
-begin
-  let K := fraction_ring R,
-  let L := fraction_ring S,
-  let P₁ := P.prim_part,
-  suffices : minpoly R s ∣ P₁,
-  { exact dvd_trans this (prim_part_dvd _) },
-  apply (is_primitive.dvd_iff_fraction_map_dvd_fraction_map K (monic hs).is_primitive
-    P.is_primitive_prim_part).2,
-  let y := algebra_map S L s,
-  have hy : is_integral R y := hs.algebra_map,
-  rw [← gcd_domain_eq_field_fractions K L hs],
-  refine dvd _ _ _,
-  rw [aeval_map_algebra_map, aeval_algebra_map_apply, aeval_prim_part_eq_zero hP hroot, map_zero]
-end
-
 variable [is_integrally_closed R]
 
 /-- For integrally closed rings, the minimal polynomial divides any polynomial that has the
   integral element as root. See also `minpoly.dvd` which relaxes the assumptions on `S`
   in exchange for stronger assumptions on `R`. -/
-theorem is_integrally_closed_dvd [nontrivial R] (p : R[X]) {s : S} (hs : is_integral R s) :
-  polynomial.aeval s p = 0 ↔ minpoly R s ∣ p :=
+theorem is_integrally_closed_dvd [nontrivial R] {s : S} (hs : is_integral R s) {p : R[X]}
+  (hp : polynomial.aeval s p = 0) : minpoly R s ∣ p :=
 begin
-  refine ⟨λ hp, _, λ hp, _⟩,
-
-  { let K := fraction_ring R,
+  let K := fraction_ring R,
     let L := fraction_ring S,
     have : minpoly K (algebra_map S L s) ∣ map (algebra_map R K) (p %ₘ (minpoly R s)),
     { rw [map_mod_by_monic _ (minpoly.monic hs), mod_by_monic_eq_sub_mul_div],
@@ -183,30 +87,27 @@ begin
       rw [← is_scalar_tower.algebra_map_eq, ← is_scalar_tower.algebra_map_eq],
 
       apply dvd_mul_of_dvd_left,
-      rw is_integrally_closed_eq_field_fractions'' K L hs,
+      rw is_integrally_closed_eq_field_fractions K L hs,
 
       exact monic.map _ (minpoly.monic hs) },
-    rw [is_integrally_closed_eq_field_fractions'' _ _ hs, map_dvd_map (algebra_map R K)
+    rw [is_integrally_closed_eq_field_fractions _ _ hs, map_dvd_map (algebra_map R K)
       (is_fraction_ring.injective R K) (minpoly.monic hs)] at this,
     rw [← dvd_iff_mod_by_monic_eq_zero (minpoly.monic hs)],
     refine polynomial.eq_zero_of_dvd_of_degree_lt this
       (degree_mod_by_monic_lt p $ minpoly.monic hs),
-      all_goals { apply_instance } },
-
-  { simpa only [ring_hom.mem_ker, ring_hom.coe_comp, coe_eval_ring_hom,
-      coe_map_ring_hom, function.comp_app, eval_map, ← aeval_def] using
-      aeval_eq_zero_of_dvd_aeval_eq_zero hp (minpoly.aeval R s) }
+      all_goals { apply_instance }
 end
 
+theorem is_integrally_closed_dvd_iff [nontrivial R] {s : S} (hs : is_integral R s) (p : R[X]) :
+  polynomial.aeval s p = 0 ↔  minpoly R s ∣ p :=
+⟨λ hp, is_integrally_closed_dvd hs hp, λ hp, by simpa only [ring_hom.mem_ker, ring_hom.coe_comp,
+  coe_eval_ring_hom, coe_map_ring_hom, function.comp_app, eval_map, ← aeval_def] using
+    aeval_eq_zero_of_dvd_aeval_eq_zero hp (minpoly.aeval R s)⟩
+
 lemma ker_eval {s : S} (hs : is_integral R s) :
   ((polynomial.aeval s).to_ring_hom : R[X] →+* S).ker = ideal.span ({minpoly R s} : set R[X] ):=
-begin
-  apply le_antisymm; intros p hp,
-  { rwa [ring_hom.mem_ker, alg_hom.to_ring_hom_eq_coe, alg_hom.coe_to_ring_hom,
-      is_integrally_closed_dvd p hs, ← ideal.mem_span_singleton] at hp },
-  { rwa [ring_hom.mem_ker, alg_hom.to_ring_hom_eq_coe, alg_hom.coe_to_ring_hom,
-      is_integrally_closed_dvd p hs, ← ideal.mem_span_singleton] }
-end
+by ext p ; simp_rw [ring_hom.mem_ker, alg_hom.to_ring_hom_eq_coe, alg_hom.coe_to_ring_hom,
+  is_integrally_closed_dvd_iff hs, ← ideal.mem_span_singleton]
 
 /-- If an element `x` is a root of a nonzero polynomial `p`, then the degree of `p` is at least the
 degree of the minimal polynomial of `x`. See also `minpoly.degree_le_of_ne_zero` which relaxes the
@@ -216,7 +117,7 @@ lemma is_integrally_closed.degree_le_of_ne_zero {s : S} (hs : is_integral R s) {
 begin
   rw [degree_eq_nat_degree (minpoly.ne_zero hs), degree_eq_nat_degree hp0],
   norm_cast,
-  exact nat_degree_le_of_dvd ((is_integrally_closed_dvd _ hs).mp hp) hp0
+  exact nat_degree_le_of_dvd ((is_integrally_closed_dvd_iff hs _).mp hp) hp0
 end
 
 /-- The minimal polynomial of an element `x` is uniquely characterized by its defining property:
@@ -255,7 +156,7 @@ begin
   by_cases hPzero : P = 0,
   { simpa [hPzero] using hP.symm },
   rw [← hP, minpoly.to_adjoin_apply', lift_hom_mk,  ← subalgebra.coe_eq_zero,
-    aeval_subalgebra_coe, set_like.coe_mk, is_integrally_closed_dvd _ hx] at hP₁,
+    aeval_subalgebra_coe, set_like.coe_mk, is_integrally_closed_dvd_iff hx] at hP₁,
   obtain ⟨Q, hQ⟩ := hP₁,
   rw [← hP, hQ, ring_hom.map_mul, mk_self, zero_mul],
 end
diff --git a/src/number_theory/cyclotomic/discriminant.lean b/src/number_theory/cyclotomic/discriminant.lean
index f268b04516fcd..2a254dc3a5519 100644
--- a/src/number_theory/cyclotomic/discriminant.lean
+++ b/src/number_theory/cyclotomic/discriminant.lean
@@ -44,9 +44,9 @@ begin
     (λ i j, to_matrix_is_integral H₁ _ _ _ _)
     (λ i j, to_matrix_is_integral H₂ _ _ _ _),
   { exact hζ.is_integral n.pos },
-  { refine minpoly.gcd_domain_eq_field_fractions' _ (hζ.is_integral n.pos) },
+  { refine minpoly.is_integrally_closed_eq_field_fractions' _ (hζ.is_integral n.pos) },
   { exact is_integral_sub (hζ.is_integral n.pos) is_integral_one },
-  { refine minpoly.gcd_domain_eq_field_fractions' _ _,
+  { refine minpoly.is_integrally_closed_eq_field_fractions' _ _,
     exact is_integral_sub (hζ.is_integral n.pos) is_integral_one }
 end
 
diff --git a/src/number_theory/cyclotomic/rat.lean b/src/number_theory/cyclotomic/rat.lean
index 67def7f2ff0c1..b7f1fdd822374 100644
--- a/src/number_theory/cyclotomic/rat.lean
+++ b/src/number_theory/cyclotomic/rat.lean
@@ -5,7 +5,7 @@ Authors: Riccardo Brasca
 -/
 
 import number_theory.cyclotomic.discriminant
-import ring_theory.polynomial.eisenstein
+import ring_theory.polynomial.eisenstein.is_integral
 
 /-!
 # Ring of integers of `p ^ n`-th cyclotomic fields
@@ -105,7 +105,7 @@ begin
     rw [← hz, ← is_scalar_tower.algebra_map_apply],
     exact subalgebra.algebra_map_mem  _ _ },
   { have hmin : (minpoly ℤ B.gen).is_eisenstein_at (submodule.span ℤ {((p : ℕ) : ℤ)}),
-    { have h₁ := minpoly.gcd_domain_eq_field_fractions' ℚ hint,
+    { have h₁ := minpoly.is_integrally_closed_eq_field_fractions' ℚ hint,
       have h₂ := hζ.minpoly_sub_one_eq_cyclotomic_comp
         (cyclotomic.irreducible_rat (p ^ _).pos),
       rw [is_primitive_root.sub_one_power_basis_gen] at h₁,
diff --git a/src/number_theory/number_field/embeddings.lean b/src/number_theory/number_field/embeddings.lean
index 3e5e993c7678b..def8c20de89d5 100644
--- a/src/number_theory/number_field/embeddings.lean
+++ b/src/number_theory/number_field/embeddings.lean
@@ -6,7 +6,7 @@ Authors: Alex J. Best, Xavier Roblot
 
 import analysis.complex.polynomial
 import data.complex.basic
-import field_theory.minpoly.gcd_monoid
+import field_theory.minpoly.is_integrally_closed
 import number_theory.number_field.basic
 
 /-!
@@ -101,7 +101,7 @@ begin
   let C := nat.ceil ((max B 1) ^ (finrank ℚ K) * (finrank ℚ K).choose ((finrank ℚ K) / 2)),
   have := bUnion_roots_finite (algebra_map ℤ K) (finrank ℚ K) (finite_Icc (-C : ℤ) C),
   refine this.subset (λ x hx, _), simp_rw mem_Union,
-  have h_map_ℚ_minpoly := minpoly.gcd_domain_eq_field_fractions' ℚ hx.1,
+  have h_map_ℚ_minpoly := minpoly.is_integrally_closed_eq_field_fractions' ℚ hx.1,
   refine ⟨_, ⟨_, λ i, _⟩, mem_root_set.2 ⟨minpoly.ne_zero hx.1, minpoly.aeval ℤ x⟩⟩,
   { rw [← (minpoly.monic hx.1).nat_degree_map (algebra_map ℤ ℚ), ← h_map_ℚ_minpoly],
     exact minpoly.nat_degree_le (is_integral_of_is_scalar_tower hx.1) },
diff --git a/src/ring_theory/dedekind_domain/adic_valuation.lean b/src/ring_theory/dedekind_domain/adic_valuation.lean
index 5098e9e5faf79..ea551209d81bb 100644
--- a/src/ring_theory/dedekind_domain/adic_valuation.lean
+++ b/src/ring_theory/dedekind_domain/adic_valuation.lean
@@ -6,6 +6,7 @@ Authors: María Inés de Frutos-Fernández
 import ring_theory.dedekind_domain.ideal
 import ring_theory.valuation.extend_to_localization
 import ring_theory.valuation.valuation_subring
+import ring_theory.polynomial.cyclotomic.basic
 import topology.algebra.valued_field
 
 /-!
diff --git a/src/ring_theory/dedekind_domain/selmer_group.lean b/src/ring_theory/dedekind_domain/selmer_group.lean
index 433814c96a50e..f729e75d1c898 100644
--- a/src/ring_theory/dedekind_domain/selmer_group.lean
+++ b/src/ring_theory/dedekind_domain/selmer_group.lean
@@ -6,6 +6,7 @@ Authors: David Kurniadi Angdinata
 import algebra.hom.equiv.type_tags
 import data.zmod.quotient
 import ring_theory.dedekind_domain.adic_valuation
+import ring_theory.norm
 
 /-!
 # Selmer groups of fraction fields of Dedekind domains
diff --git a/src/ring_theory/is_adjoin_root.lean b/src/ring_theory/is_adjoin_root.lean
index a9d74b7173734..766e7a34bfebb 100644
--- a/src/ring_theory/is_adjoin_root.lean
+++ b/src/ring_theory/is_adjoin_root.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anne Baanen
 -/
 import data.polynomial.algebra_map
-import field_theory.minpoly.gcd_monoid
+import field_theory.minpoly.is_integrally_closed
 import ring_theory.power_basis
 
 /-!
@@ -627,10 +627,10 @@ end is_adjoin_root
 
 namespace is_adjoin_root_monic
 
-lemma minpoly_eq [is_domain R] [is_domain S] [no_zero_smul_divisors R S] [normalized_gcd_monoid R]
+lemma minpoly_eq [is_domain R] [is_domain S] [no_zero_smul_divisors R S] [is_integrally_closed R]
   (h : is_adjoin_root_monic S f) (hirr : irreducible f) :
   minpoly R h.root = f :=
-let ⟨q, hq⟩ := minpoly.gcd_domain_dvd h.is_integral_root h.monic.ne_zero h.aeval_root in
+let ⟨q, hq⟩ := minpoly.is_integrally_closed_dvd h.is_integral_root h.aeval_root in
 symm $ eq_of_monic_of_associated h.monic (minpoly.monic h.is_integral_root) $
 by convert (associated.mul_left (minpoly R h.root) $
     associated_one_iff_is_unit.2 $ (hirr.is_unit_or_is_unit hq).resolve_left $
diff --git a/src/ring_theory/polynomial/cyclotomic/basic.lean b/src/ring_theory/polynomial/cyclotomic/basic.lean
index 141cc8845711e..90332b2db71e3 100644
--- a/src/ring_theory/polynomial/cyclotomic/basic.lean
+++ b/src/ring_theory/polynomial/cyclotomic/basic.lean
@@ -787,7 +787,7 @@ lemma _root_.is_primitive_root.minpoly_dvd_cyclotomic {n : ℕ} {K : Type*} [fie
   (h : is_primitive_root μ n) (hpos : 0 < n) [char_zero K] :
   minpoly ℤ μ ∣ cyclotomic n ℤ :=
 begin
-  apply minpoly.gcd_domain_dvd (is_integral h hpos) (cyclotomic_ne_zero n ℤ),
+  apply minpoly.is_integrally_closed_dvd (is_integral h hpos),
   simpa [aeval_def, eval₂_eq_eval_map, is_root.def] using is_root_cyclotomic hpos h
 end
 
@@ -816,7 +816,7 @@ lemma cyclotomic_eq_minpoly_rat {n : ℕ} {K : Type*} [field K] {μ : K}
   cyclotomic n ℚ = minpoly ℚ μ :=
 begin
   rw [← map_cyclotomic_int, cyclotomic_eq_minpoly h hpos],
-  exact (minpoly.gcd_domain_eq_field_fractions' _ (is_integral h hpos)).symm
+  exact (minpoly.is_integrally_closed_eq_field_fractions' _ (is_integral h hpos)).symm
 end
 
 /-- `cyclotomic n ℤ` is irreducible. -/
@@ -909,8 +909,7 @@ begin
   { have hpos := nat.mul_pos hzero hp.pos,
     have hprim := complex.is_primitive_root_exp _ hpos.ne.symm,
     rw [cyclotomic_eq_minpoly hprim hpos],
-    refine minpoly.gcd_domain_dvd (hprim.is_integral hpos)
-      ((cyclotomic.monic n ℤ).expand hp.pos).ne_zero _,
+    refine minpoly.is_integrally_closed_dvd (hprim.is_integral hpos) _,
     rw [aeval_def, ← eval_map, map_expand, map_cyclotomic, expand_eval,
         ← is_root.def, is_root_cyclotomic_iff],
     { convert is_primitive_root.pow_of_dvd hprim hp.ne_zero (dvd_mul_left p n),
diff --git a/src/ring_theory/polynomial/eisenstein/basic.lean b/src/ring_theory/polynomial/eisenstein/basic.lean
new file mode 100644
index 0000000000000..6d37190e8da92
--- /dev/null
+++ b/src/ring_theory/polynomial/eisenstein/basic.lean
@@ -0,0 +1,233 @@
+/-
+Copyright (c) 2022 Riccardo Brasca. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Riccardo Brasca
+-/
+
+import ring_theory.eisenstein_criterion
+import ring_theory.polynomial.scale_roots
+
+/-!
+# Eisenstein polynomials
+Given an ideal `𝓟` of a commutative semiring `R`, we say that a polynomial `f : R[X]` is
+*Eisenstein at `𝓟`* if `f.leading_coeff ∉ 𝓟`, `∀ n, n < f.nat_degree → f.coeff n ∈ 𝓟` and
+`f.coeff 0 ∉ 𝓟 ^ 2`. In this file we gather miscellaneous results about Eisenstein polynomials.
+
+## Main definitions
+* `polynomial.is_eisenstein_at f 𝓟`: the property of being Eisenstein at `𝓟`.
+
+## Main results
+* `polynomial.is_eisenstein_at.irreducible`: if a primitive `f` satisfies `f.is_eisenstein_at 𝓟`,
+  where `𝓟.is_prime`, then `f` is irreducible.
+
+## Implementation details
+We also define a notion `is_weakly_eisenstein_at` requiring only that
+`∀ n < f.nat_degree → f.coeff n ∈ 𝓟`. This makes certain results slightly more general and it is
+useful since it is sometimes better behaved (for example it is stable under `polynomial.map`).
+
+-/
+
+universes u v w z
+
+variables {R : Type u}
+
+open ideal algebra finset
+
+open_locale big_operators polynomial
+
+namespace polynomial
+
+/-- Given an ideal `𝓟` of a commutative semiring `R`, we say that a polynomial `f : R[X]`
+is *weakly Eisenstein at `𝓟`* if `∀ n, n < f.nat_degree → f.coeff n ∈ 𝓟`. -/
+@[mk_iff] structure is_weakly_eisenstein_at [comm_semiring R] (f : R[X]) (𝓟 : ideal R) :
+  Prop := (mem : ∀ {n}, n < f.nat_degree → f.coeff n ∈ 𝓟)
+
+/-- Given an ideal `𝓟` of a commutative semiring `R`, we say that a polynomial `f : R[X]`
+is *Eisenstein at `𝓟`* if `f.leading_coeff ∉ 𝓟`, `∀ n, n < f.nat_degree → f.coeff n ∈ 𝓟` and
+`f.coeff 0 ∉ 𝓟 ^ 2`. -/
+@[mk_iff] structure is_eisenstein_at [comm_semiring R] (f : R[X]) (𝓟 : ideal R) : Prop :=
+(leading : f.leading_coeff ∉ 𝓟)
+(mem : ∀ {n}, n < f.nat_degree → f.coeff n ∈ 𝓟)
+(not_mem : f.coeff 0 ∉ 𝓟 ^ 2)
+
+namespace is_weakly_eisenstein_at
+
+section comm_semiring
+
+variables [comm_semiring R] {𝓟 : ideal R} {f : R[X]} (hf : f.is_weakly_eisenstein_at 𝓟)
+
+include hf
+
+lemma map {A : Type v} [comm_ring A] (φ : R →+* A) : (f.map φ).is_weakly_eisenstein_at (𝓟.map φ) :=
+begin
+  refine (is_weakly_eisenstein_at_iff _ _).2 (λ n hn, _),
+  rw [coeff_map],
+  exact mem_map_of_mem _ (hf.mem (lt_of_lt_of_le hn (nat_degree_map_le _ _)))
+end
+
+end comm_semiring
+
+section comm_ring
+
+variables [comm_ring R] {𝓟 : ideal R} {f : R[X]} (hf : f.is_weakly_eisenstein_at 𝓟)
+variables {S : Type v} [comm_ring S] [algebra R S]
+
+section principal
+
+variable {p : R}
+
+local notation `P` := submodule.span R {p}
+
+lemma exists_mem_adjoin_mul_eq_pow_nat_degree {x : S} (hx : aeval x f = 0)
+  (hmo : f.monic) (hf : f.is_weakly_eisenstein_at P) : ∃ y ∈ adjoin R ({x} : set S),
+  (algebra_map R S) p * y = x ^ (f.map (algebra_map R S)).nat_degree :=
+begin
+  rw [aeval_def, polynomial.eval₂_eq_eval_map, eval_eq_sum_range, range_add_one,
+    sum_insert not_mem_range_self, sum_range, (hmo.map
+    (algebra_map R S)).coeff_nat_degree, one_mul] at hx,
+  replace hx := eq_neg_of_add_eq_zero_left hx,
+  have : ∀ n < f.nat_degree, p ∣ f.coeff n,
+  { intros n hn,
+    refine mem_span_singleton.1 (by simpa using hf.mem hn) },
+  choose! φ hφ using this,
+  conv_rhs at hx { congr, congr, skip, funext,
+    rw [fin.coe_eq_val, coeff_map, hφ i.1 (lt_of_lt_of_le i.2 (nat_degree_map_le _ _)),
+      ring_hom.map_mul, mul_assoc] },
+  rw [hx, ← mul_sum, neg_eq_neg_one_mul, ← mul_assoc (-1 : S), mul_comm (-1 : S), mul_assoc],
+  refine ⟨-1 * ∑ (i : fin (f.map (algebra_map R S)).nat_degree),
+    (algebra_map R S) (φ i.1) * x ^ i.1, _, rfl⟩,
+  exact subalgebra.mul_mem _ (subalgebra.neg_mem _ (subalgebra.one_mem _))
+    (subalgebra.sum_mem _ (λ i hi, subalgebra.mul_mem _ (subalgebra.algebra_map_mem _ _)
+    (subalgebra.pow_mem _ (subset_adjoin (set.mem_singleton x)) _)))
+end
+
+lemma exists_mem_adjoin_mul_eq_pow_nat_degree_le {x : S} (hx : aeval x f = 0)
+  (hmo : f.monic) (hf : f.is_weakly_eisenstein_at P) :
+  ∀ i, (f.map (algebra_map R S)).nat_degree ≤ i →
+  ∃ y ∈ adjoin R ({x} : set S), (algebra_map R S) p * y = x ^ i :=
+begin
+  intros i hi,
+  obtain ⟨k, hk⟩ := exists_add_of_le hi,
+  rw [hk, pow_add],
+  obtain ⟨y, hy, H⟩ := exists_mem_adjoin_mul_eq_pow_nat_degree hx hmo hf,
+  refine ⟨y * x ^ k, _, _⟩,
+  { exact subalgebra.mul_mem _ hy (subalgebra.pow_mem _  (subset_adjoin (set.mem_singleton x)) _) },
+  { rw [← mul_assoc _ y, H] }
+end
+
+end principal
+
+include hf
+
+lemma pow_nat_degree_le_of_root_of_monic_mem {x : R} (hroot : is_root f x) (hmo : f.monic) :
+  ∀ i, f.nat_degree ≤ i → x ^ i ∈ 𝓟 :=
+begin
+  intros i hi,
+  obtain ⟨k, hk⟩ := exists_add_of_le hi,
+  rw [hk, pow_add],
+  suffices : x ^ f.nat_degree ∈ 𝓟,
+  { exact mul_mem_right (x ^ k) 𝓟 this },
+  rw [is_root.def, eval_eq_sum_range, finset.range_add_one, finset.sum_insert
+    finset.not_mem_range_self, finset.sum_range, hmo.coeff_nat_degree, one_mul] at hroot,
+  rw [eq_neg_of_add_eq_zero_left hroot, neg_mem_iff],
+  refine submodule.sum_mem _ (λ i hi,  mul_mem_right _ _ (hf.mem (fin.is_lt i)))
+end
+
+lemma pow_nat_degree_le_of_aeval_zero_of_monic_mem_map {x : S} (hx : aeval x f = 0)
+  (hmo : f.monic) :
+  ∀ i, (f.map (algebra_map R S)).nat_degree ≤ i → x ^ i ∈ 𝓟.map (algebra_map R S) :=
+begin
+  suffices : x ^ (f.map (algebra_map R S)).nat_degree ∈ 𝓟.map (algebra_map R S),
+  { intros i hi,
+    obtain ⟨k, hk⟩ := exists_add_of_le hi,
+    rw [hk, pow_add],
+    refine mul_mem_right _ _ this },
+  rw [aeval_def, eval₂_eq_eval_map, ← is_root.def] at hx,
+  refine pow_nat_degree_le_of_root_of_monic_mem (hf.map _) hx (hmo.map _) _ rfl.le
+end
+
+end comm_ring
+
+end is_weakly_eisenstein_at
+
+section scale_roots
+
+variables {A : Type*} [comm_ring R] [comm_ring A]
+
+lemma scale_roots.is_weakly_eisenstein_at (p : R[X]) {x : R}
+  {P : ideal R} (hP : x ∈ P) : (scale_roots p x).is_weakly_eisenstein_at P :=
+begin
+  refine ⟨λ i hi, _⟩,
+  rw coeff_scale_roots,
+  rw [nat_degree_scale_roots, ← tsub_pos_iff_lt] at hi,
+  exact ideal.mul_mem_left _ _ (ideal.pow_mem_of_mem P hP _ hi)
+end
+
+lemma dvd_pow_nat_degree_of_eval₂_eq_zero {f : R →+* A}
+  (hf : function.injective f) {p : R[X]} (hp : p.monic) (x y : R) (z : A)
+  (h : p.eval₂ f z = 0) (hz : f x * z = f y) : x ∣ y ^ p.nat_degree :=
+begin
+  rw [← nat_degree_scale_roots p x, ← ideal.mem_span_singleton],
+  refine (scale_roots.is_weakly_eisenstein_at _ (ideal.mem_span_singleton.mpr $ dvd_refl x))
+    .pow_nat_degree_le_of_root_of_monic_mem _ ((monic_scale_roots_iff x).mpr hp) _ le_rfl,
+  rw injective_iff_map_eq_zero' at hf,
+  have := scale_roots_eval₂_eq_zero f h,
+  rwa [hz, polynomial.eval₂_at_apply, hf] at this
+end
+
+lemma dvd_pow_nat_degree_of_aeval_eq_zero [algebra R A] [nontrivial A]
+  [no_zero_smul_divisors R A] {p : R[X]} (hp : p.monic) (x y : R) (z : A)
+  (h : polynomial.aeval z p = 0) (hz : z * algebra_map R A x = algebra_map R A y) :
+  x ∣ y ^ p.nat_degree :=
+dvd_pow_nat_degree_of_eval₂_eq_zero (no_zero_smul_divisors.algebra_map_injective R A)
+  hp x y z h ((mul_comm _ _).trans hz)
+
+end scale_roots
+
+namespace is_eisenstein_at
+
+section comm_semiring
+
+variables [comm_semiring R] {𝓟 : ideal R} {f : R[X]} (hf : f.is_eisenstein_at 𝓟)
+
+lemma _root_.polynomial.monic.leading_coeff_not_mem (hf : f.monic) (h : 𝓟 ≠ ⊤) :
+  ¬f.leading_coeff ∈ 𝓟 :=
+hf.leading_coeff.symm ▸ (ideal.ne_top_iff_one _).1 h
+
+lemma _root_.polynomial.monic.is_eisenstein_at_of_mem_of_not_mem (hf : f.monic) (h : 𝓟 ≠ ⊤)
+  (hmem : ∀ {n}, n < f.nat_degree → f.coeff n ∈ 𝓟) (hnot_mem : f.coeff 0 ∉ 𝓟 ^ 2) :
+  f.is_eisenstein_at 𝓟 :=
+{ leading := hf.leading_coeff_not_mem h,
+  mem := λ n hn, hmem hn,
+  not_mem := hnot_mem }
+
+include hf
+
+lemma is_weakly_eisenstein_at : is_weakly_eisenstein_at f 𝓟 := ⟨λ _, hf.mem⟩
+
+lemma coeff_mem {n : ℕ} (hn : n ≠ f.nat_degree) : f.coeff n ∈ 𝓟 :=
+begin
+  cases ne_iff_lt_or_gt.1 hn,
+  { exact hf.mem h },
+  { rw [coeff_eq_zero_of_nat_degree_lt h],
+    exact ideal.zero_mem _}
+end
+
+end comm_semiring
+
+section is_domain
+
+variables [comm_ring R] [is_domain R] {𝓟 : ideal R} {f : R[X]} (hf : f.is_eisenstein_at 𝓟)
+
+/-- If a primitive `f` satisfies `f.is_eisenstein_at 𝓟`, where `𝓟.is_prime`, then `f` is
+irreducible. -/
+lemma irreducible (hprime : 𝓟.is_prime) (hu : f.is_primitive)
+  (hfd0 : 0 < f.nat_degree) : irreducible f :=
+irreducible_of_eisenstein_criterion hprime hf.leading (λ n hn, hf.mem (coe_lt_degree.1 hn))
+  (nat_degree_pos_iff_degree_pos.1 hfd0) hf.not_mem hu
+
+end is_domain
+
+end is_eisenstein_at
+
+end polynomial
diff --git a/src/ring_theory/polynomial/eisenstein.lean b/src/ring_theory/polynomial/eisenstein/is_integral.lean
similarity index 68%
rename from src/ring_theory/polynomial/eisenstein.lean
rename to src/ring_theory/polynomial/eisenstein/is_integral.lean
index e1c05e1080d69..9287f49e81052 100644
--- a/src/ring_theory/polynomial/eisenstein.lean
+++ b/src/ring_theory/polynomial/eisenstein/is_integral.lean
@@ -4,23 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Riccardo Brasca
 -/
 
-import ring_theory.eisenstein_criterion
 import ring_theory.integrally_closed
 import ring_theory.norm
 import ring_theory.polynomial.cyclotomic.basic
 
 /-!
 # Eisenstein polynomials
-Given an ideal `𝓟` of a commutative semiring `R`, we say that a polynomial `f : R[X]` is
-*Eisenstein at `𝓟`* if `f.leading_coeff ∉ 𝓟`, `∀ n, n < f.nat_degree → f.coeff n ∈ 𝓟` and
-`f.coeff 0 ∉ 𝓟 ^ 2`. In this file we gather miscellaneous results about Eisenstein polynomials.
-
-## Main definitions
-* `polynomial.is_eisenstein_at f 𝓟`: the property of being Eisenstein at `𝓟`.
+In this file we gather more miscellaneous results about Eisenstein polynomials
 
 ## Main results
-* `polynomial.is_eisenstein_at.irreducible`: if a primitive `f` satisfies `f.is_eisenstein_at 𝓟`,
-  where `𝓟.is_prime`, then `f` is irreducible.
 * `mem_adjoin_of_smul_prime_pow_smul_of_minpoly_is_eiseinstein_at`: let `K` be the field of fraction
   of an integrally closed domain `R` and let `L` be a separable extension of `K`, generated by an
   integral power basis `B` such that the minimal polynomial of `B.gen` is Eisenstein at `p`. Given
@@ -28,11 +20,6 @@ Given an ideal `𝓟` of a commutative semiring `R`, we say that a polynomial `f
   Together with `algebra.discr_mul_is_integral_mem_adjoin` this result often allows to compute the
   ring of integers of `L`.
 
-## Implementation details
-We also define a notion `is_weakly_eisenstein_at` requiring only that
-`∀ n < f.nat_degree → f.coeff n ∈ 𝓟`. This makes certain results slightly more general and it is
-useful since it is sometimes better behaved (for example it is stable under `polynomial.map`).
-
 -/
 
 universes u v w z
@@ -43,203 +30,6 @@ open ideal algebra finset
 
 open_locale big_operators polynomial
 
-namespace polynomial
-
-/-- Given an ideal `𝓟` of a commutative semiring `R`, we say that a polynomial `f : R[X]`
-is *weakly Eisenstein at `𝓟`* if `∀ n, n < f.nat_degree → f.coeff n ∈ 𝓟`. -/
-@[mk_iff] structure is_weakly_eisenstein_at [comm_semiring R] (f : R[X]) (𝓟 : ideal R) :
-  Prop := (mem : ∀ {n}, n < f.nat_degree → f.coeff n ∈ 𝓟)
-
-/-- Given an ideal `𝓟` of a commutative semiring `R`, we say that a polynomial `f : R[X]`
-is *Eisenstein at `𝓟`* if `f.leading_coeff ∉ 𝓟`, `∀ n, n < f.nat_degree → f.coeff n ∈ 𝓟` and
-`f.coeff 0 ∉ 𝓟 ^ 2`. -/
-@[mk_iff] structure is_eisenstein_at [comm_semiring R] (f : R[X]) (𝓟 : ideal R) : Prop :=
-(leading : f.leading_coeff ∉ 𝓟)
-(mem : ∀ {n}, n < f.nat_degree → f.coeff n ∈ 𝓟)
-(not_mem : f.coeff 0 ∉ 𝓟 ^ 2)
-
-namespace is_weakly_eisenstein_at
-
-section comm_semiring
-
-variables [comm_semiring R] {𝓟 : ideal R} {f : R[X]} (hf : f.is_weakly_eisenstein_at 𝓟)
-
-include hf
-
-lemma map {A : Type v} [comm_ring A] (φ : R →+* A) : (f.map φ).is_weakly_eisenstein_at (𝓟.map φ) :=
-begin
-  refine (is_weakly_eisenstein_at_iff _ _).2 (λ n hn, _),
-  rw [coeff_map],
-  exact mem_map_of_mem _ (hf.mem (lt_of_lt_of_le hn (nat_degree_map_le _ _)))
-end
-
-end comm_semiring
-
-section comm_ring
-
-variables [comm_ring R] {𝓟 : ideal R} {f : R[X]} (hf : f.is_weakly_eisenstein_at 𝓟)
-variables {S : Type v} [comm_ring S] [algebra R S]
-
-section principal
-
-variable {p : R}
-
-local notation `P` := submodule.span R {p}
-
-lemma exists_mem_adjoin_mul_eq_pow_nat_degree {x : S} (hx : aeval x f = 0)
-  (hmo : f.monic) (hf : f.is_weakly_eisenstein_at P) : ∃ y ∈ adjoin R ({x} : set S),
-  (algebra_map R S) p * y = x ^ (f.map (algebra_map R S)).nat_degree :=
-begin
-  rw [aeval_def, polynomial.eval₂_eq_eval_map, eval_eq_sum_range, range_add_one,
-    sum_insert not_mem_range_self, sum_range, (hmo.map
-    (algebra_map R S)).coeff_nat_degree, one_mul] at hx,
-  replace hx := eq_neg_of_add_eq_zero_left hx,
-  have : ∀ n < f.nat_degree, p ∣ f.coeff n,
-  { intros n hn,
-    refine mem_span_singleton.1 (by simpa using hf.mem hn) },
-  choose! φ hφ using this,
-  conv_rhs at hx { congr, congr, skip, funext,
-    rw [fin.coe_eq_val, coeff_map, hφ i.1 (lt_of_lt_of_le i.2 (nat_degree_map_le _ _)),
-      ring_hom.map_mul, mul_assoc] },
-  rw [hx, ← mul_sum, neg_eq_neg_one_mul, ← mul_assoc (-1 : S), mul_comm (-1 : S), mul_assoc],
-  refine ⟨-1 * ∑ (i : fin (f.map (algebra_map R S)).nat_degree),
-    (algebra_map R S) (φ i.1) * x ^ i.1, _, rfl⟩,
-  exact subalgebra.mul_mem _ (subalgebra.neg_mem _ (subalgebra.one_mem _))
-    (subalgebra.sum_mem _ (λ i hi, subalgebra.mul_mem _ (subalgebra.algebra_map_mem _ _)
-    (subalgebra.pow_mem _ (subset_adjoin (set.mem_singleton x)) _)))
-end
-
-lemma exists_mem_adjoin_mul_eq_pow_nat_degree_le {x : S} (hx : aeval x f = 0)
-  (hmo : f.monic) (hf : f.is_weakly_eisenstein_at P) :
-  ∀ i, (f.map (algebra_map R S)).nat_degree ≤ i →
-  ∃ y ∈ adjoin R ({x} : set S), (algebra_map R S) p * y = x ^ i :=
-begin
-  intros i hi,
-  obtain ⟨k, hk⟩ := exists_add_of_le hi,
-  rw [hk, pow_add],
-  obtain ⟨y, hy, H⟩ := exists_mem_adjoin_mul_eq_pow_nat_degree hx hmo hf,
-  refine ⟨y * x ^ k, _, _⟩,
-  { exact subalgebra.mul_mem _ hy (subalgebra.pow_mem _  (subset_adjoin (set.mem_singleton x)) _) },
-  { rw [← mul_assoc _ y, H] }
-end
-
-end principal
-
-include hf
-
-lemma pow_nat_degree_le_of_root_of_monic_mem {x : R} (hroot : is_root f x) (hmo : f.monic) :
-  ∀ i, f.nat_degree ≤ i → x ^ i ∈ 𝓟 :=
-begin
-  intros i hi,
-  obtain ⟨k, hk⟩ := exists_add_of_le hi,
-  rw [hk, pow_add],
-  suffices : x ^ f.nat_degree ∈ 𝓟,
-  { exact mul_mem_right (x ^ k) 𝓟 this },
-  rw [is_root.def, eval_eq_sum_range, finset.range_add_one, finset.sum_insert
-    finset.not_mem_range_self, finset.sum_range, hmo.coeff_nat_degree, one_mul] at hroot,
-  rw [eq_neg_of_add_eq_zero_left hroot, neg_mem_iff],
-  refine submodule.sum_mem _ (λ i hi,  mul_mem_right _ _ (hf.mem (fin.is_lt i)))
-end
-
-lemma pow_nat_degree_le_of_aeval_zero_of_monic_mem_map {x : S} (hx : aeval x f = 0)
-  (hmo : f.monic) :
-  ∀ i, (f.map (algebra_map R S)).nat_degree ≤ i → x ^ i ∈ 𝓟.map (algebra_map R S) :=
-begin
-  suffices : x ^ (f.map (algebra_map R S)).nat_degree ∈ 𝓟.map (algebra_map R S),
-  { intros i hi,
-    obtain ⟨k, hk⟩ := exists_add_of_le hi,
-    rw [hk, pow_add],
-    refine mul_mem_right _ _ this },
-  rw [aeval_def, eval₂_eq_eval_map, ← is_root.def] at hx,
-  refine pow_nat_degree_le_of_root_of_monic_mem (hf.map _) hx (hmo.map _) _ rfl.le
-end
-
-end comm_ring
-
-end is_weakly_eisenstein_at
-
-section scale_roots
-
-variables {A : Type*} [comm_ring R] [comm_ring A]
-
-lemma scale_roots.is_weakly_eisenstein_at (p : R[X]) {x : R}
-  {P : ideal R} (hP : x ∈ P) : (scale_roots p x).is_weakly_eisenstein_at P :=
-begin
-  refine ⟨λ i hi, _⟩,
-  rw coeff_scale_roots,
-  rw [nat_degree_scale_roots, ← tsub_pos_iff_lt] at hi,
-  exact ideal.mul_mem_left _ _ (ideal.pow_mem_of_mem P hP _ hi)
-end
-
-lemma dvd_pow_nat_degree_of_eval₂_eq_zero {f : R →+* A}
-  (hf : function.injective f) {p : R[X]} (hp : p.monic) (x y : R) (z : A)
-  (h : p.eval₂ f z = 0) (hz : f x * z = f y) : x ∣ y ^ p.nat_degree :=
-begin
-  rw [← nat_degree_scale_roots p x, ← ideal.mem_span_singleton],
-  refine (scale_roots.is_weakly_eisenstein_at _ (ideal.mem_span_singleton.mpr $ dvd_refl x))
-    .pow_nat_degree_le_of_root_of_monic_mem _ ((monic_scale_roots_iff x).mpr hp) _ le_rfl,
-  rw injective_iff_map_eq_zero' at hf,
-  have := scale_roots_eval₂_eq_zero f h,
-  rwa [hz, polynomial.eval₂_at_apply, hf] at this
-end
-
-lemma dvd_pow_nat_degree_of_aeval_eq_zero [algebra R A] [nontrivial A]
-  [no_zero_smul_divisors R A] {p : R[X]} (hp : p.monic) (x y : R) (z : A)
-  (h : polynomial.aeval z p = 0) (hz : z * algebra_map R A x = algebra_map R A y) :
-  x ∣ y ^ p.nat_degree :=
-dvd_pow_nat_degree_of_eval₂_eq_zero (no_zero_smul_divisors.algebra_map_injective R A)
-  hp x y z h ((mul_comm _ _).trans hz)
-
-end scale_roots
-
-namespace is_eisenstein_at
-
-section comm_semiring
-
-variables [comm_semiring R] {𝓟 : ideal R} {f : R[X]} (hf : f.is_eisenstein_at 𝓟)
-
-lemma _root_.polynomial.monic.leading_coeff_not_mem (hf : f.monic) (h : 𝓟 ≠ ⊤) :
-  ¬f.leading_coeff ∈ 𝓟 :=
-hf.leading_coeff.symm ▸ (ideal.ne_top_iff_one _).1 h
-
-lemma _root_.polynomial.monic.is_eisenstein_at_of_mem_of_not_mem (hf : f.monic) (h : 𝓟 ≠ ⊤)
-  (hmem : ∀ {n}, n < f.nat_degree → f.coeff n ∈ 𝓟) (hnot_mem : f.coeff 0 ∉ 𝓟 ^ 2) :
-  f.is_eisenstein_at 𝓟 :=
-{ leading := hf.leading_coeff_not_mem h,
-  mem := λ n hn, hmem hn,
-  not_mem := hnot_mem }
-
-include hf
-
-lemma is_weakly_eisenstein_at : is_weakly_eisenstein_at f 𝓟 := ⟨λ _, hf.mem⟩
-
-lemma coeff_mem {n : ℕ} (hn : n ≠ f.nat_degree) : f.coeff n ∈ 𝓟 :=
-begin
-  cases ne_iff_lt_or_gt.1 hn,
-  { exact hf.mem h },
-  { rw [coeff_eq_zero_of_nat_degree_lt h],
-    exact ideal.zero_mem _}
-end
-
-end comm_semiring
-
-section is_domain
-
-variables [comm_ring R] [is_domain R] {𝓟 : ideal R} {f : R[X]} (hf : f.is_eisenstein_at 𝓟)
-
-/-- If a primitive `f` satisfies `f.is_eisenstein_at 𝓟`, where `𝓟.is_prime`, then `f` is
-irreducible. -/
-lemma irreducible (hprime : 𝓟.is_prime) (hu : f.is_primitive)
-  (hfd0 : 0 < f.nat_degree) : irreducible f :=
-irreducible_of_eisenstein_criterion hprime hf.leading (λ n hn, hf.mem (coe_lt_degree.1 hn))
-  (nat_degree_pos_iff_degree_pos.1 hfd0) hf.not_mem hu
-
-end is_domain
-
-end is_eisenstein_at
-
-end polynomial
-
 section cyclotomic
 
 variables (p : ℕ)
@@ -329,7 +119,7 @@ section is_integral
 
 variables {K : Type v} {L : Type z} {p : R} [comm_ring R] [field K] [field L]
 variables [algebra K L] [algebra R L] [algebra R K] [is_scalar_tower R K L] [is_separable K L]
-variables [is_domain R] [normalized_gcd_monoid R] [is_fraction_ring R K] [is_integrally_closed R]
+variables [is_domain R] [is_fraction_ring R K] [is_integrally_closed R]
 
 local notation `𝓟` := submodule.span R {p}
 
@@ -351,7 +141,7 @@ begin
   have finrank_K_L : finite_dimensional.finrank K L = B.dim := B.finrank,
   have deg_K_P : (minpoly K B.gen).nat_degree = B.dim := B.nat_degree_minpoly,
   have deg_R_P : P.nat_degree = B.dim,
-  { rw [← deg_K_P, minpoly.gcd_domain_eq_field_fractions' K hBint,
+  { rw [← deg_K_P, minpoly.is_integrally_closed_eq_field_fractions' K hBint,
         (minpoly.monic hBint).nat_degree_map (algebra_map R K)] },
   choose! f hf using hei.is_weakly_eisenstein_at.exists_mem_adjoin_mul_eq_pow_nat_degree_le
     (minpoly.aeval R B.gen) (minpoly.monic hBint),
@@ -393,7 +183,7 @@ begin
   ... = _ : _,
   { simp only [algebra.smul_def, algebra_map_apply R K L, algebra.norm_algebra_map, _root_.map_mul,
       _root_.map_pow, finrank_K_L, power_basis.norm_gen_eq_coeff_zero_minpoly,
-      minpoly.gcd_domain_eq_field_fractions' K hBint, coeff_map, ← hn],
+      minpoly.is_integrally_closed_eq_field_fractions' K hBint, coeff_map, ← hn],
     ring_exp },
   swap, { simp_rw [← smul_sum, ← smul_sub, algebra.smul_def p, algebra_map_apply R K L,
       _root_.map_mul, algebra.norm_algebra_map, finrank_K_L, hr, ← hn] },
@@ -527,8 +317,8 @@ begin
     rw [nat.succ_eq_add_one, add_assoc, ← nat.add_sub_assoc H, ← add_assoc, add_comm (j + 1),
       nat.add_sub_add_left, ← nat.add_sub_assoc, nat.add_sub_add_left, hP,
       ← (minpoly.monic hBint).nat_degree_map  (algebra_map R K),
-      ← minpoly.gcd_domain_eq_field_fractions' K hBint, nat_degree_minpoly, hn, nat.sub_one,
-      nat.pred_succ],
+      ← minpoly.is_integrally_closed_eq_field_fractions' K hBint, nat_degree_minpoly, hn,
+        nat.sub_one, nat.pred_succ],
     linarith },
 
   -- Using `hQ : aeval B.gen Q = p • z`, we write `p • z` as a sum of terms of degree less than
@@ -564,8 +354,8 @@ begin
     obtain ⟨r, hr⟩ := is_integral_iff.1 (is_integral_norm K hintsum),
     rw [algebra.smul_def, mul_assoc, ← mul_sub, _root_.map_mul, algebra_map_apply R K L, map_pow,
       algebra.norm_algebra_map, _root_.map_mul, algebra_map_apply R K L, algebra.norm_algebra_map,
-      finrank B, ← hr,
-      power_basis.norm_gen_eq_coeff_zero_minpoly, minpoly.gcd_domain_eq_field_fractions' K hBint,
+      finrank B, ← hr, power_basis.norm_gen_eq_coeff_zero_minpoly,
+      minpoly.is_integrally_closed_eq_field_fractions' K hBint,
       coeff_map, show (-1 : K) = algebra_map R K (-1), by simp, ← map_pow, ← map_pow,
       ← _root_.map_mul, ← map_pow, ← _root_.map_mul, ← map_pow, ← _root_.map_mul] at hQ,
 
diff --git a/src/ring_theory/roots_of_unity.lean b/src/ring_theory/roots_of_unity.lean
index d4ba7b344f82f..c21e28e689fb0 100644
--- a/src/ring_theory/roots_of_unity.lean
+++ b/src/ring_theory/roots_of_unity.lean
@@ -6,9 +6,10 @@ Authors: Johan Commelin
 
 import algebra.char_p.two
 import algebra.ne_zero
+import algebra.gcd_monoid.integrally_closed
 import data.polynomial.ring_division
 import field_theory.finite.basic
-import field_theory.minpoly.gcd_monoid
+import field_theory.minpoly.is_integrally_closed
 import field_theory.separable
 import group_theory.specific_groups.cyclic
 import number_theory.divisors
@@ -908,7 +909,8 @@ lemma minpoly_dvd_X_pow_sub_one : minpoly ℤ μ ∣ X ^ n - 1 :=
 begin
   rcases n.eq_zero_or_pos with rfl | hpos,
   { simp },
-  apply minpoly.gcd_domain_dvd (is_integral h hpos) (monic_X_pow_sub_C 1 hpos.ne').ne_zero,
+  letI : is_integrally_closed ℤ := gcd_monoid.to_is_integrally_closed,
+  apply minpoly.is_integrally_closed_dvd (is_integral h hpos),
   simp only [((is_primitive_root.iff_def μ n).mp h).left, aeval_X_pow, eq_int_cast,
   int.cast_one, aeval_one, alg_hom.map_sub, sub_self]
 end
@@ -933,17 +935,13 @@ lemma squarefree_minpoly_mod {p : ℕ} [fact p.prime] (hdiv : ¬ p ∣ n) :
 (separable_minpoly_mod h hdiv).squarefree
 
 /- Let `P` be the minimal polynomial of a root of unity `μ` and `Q` be the minimal polynomial of
-`μ ^ p`, where `p` is a prime that does not divide `n`. Then `P` divides `expand ℤ p Q`. -/
-lemma minpoly_dvd_expand {p : ℕ} (hprime : nat.prime p) (hdiv : ¬ p ∣ n) :
-  minpoly ℤ μ ∣ expand ℤ p (minpoly ℤ (μ ^ p)) :=
+`μ ^ p`, where `p` is a natural number that does not divide `n`. Then `P` divides `expand ℤ p Q`. -/
+lemma minpoly_dvd_expand {p : ℕ} (hdiv : ¬ p ∣ n) : minpoly ℤ μ ∣ expand ℤ p (minpoly ℤ (μ ^ p)) :=
 begin
   rcases n.eq_zero_or_pos with rfl | hpos,
   { simp * at *, },
-  refine minpoly.gcd_domain_dvd (h.is_integral hpos) _ _,
-  { apply monic.ne_zero,
-    rw [polynomial.monic, leading_coeff, nat_degree_expand, mul_comm, coeff_expand_mul'
-        (nat.prime.pos hprime), ← leading_coeff, ← polynomial.monic],
-    exact minpoly.monic (is_integral (pow_of_prime h hprime hdiv) hpos) },
+  letI : is_integrally_closed ℤ := gcd_monoid.to_is_integrally_closed,
+  refine minpoly.is_integrally_closed_dvd (h.is_integral hpos) _,
   { rw [aeval_def, coe_expand, ← comp, eval₂_eq_eval_map, map_comp, polynomial.map_pow, map_X,
         eval_comp, eval_pow, eval_X, ← eval₂_eq_eval_map, ← aeval_def],
     exact minpoly.aeval _ _ }
@@ -961,7 +959,7 @@ begin
   by rw [← zmod.expand_card, map_expand],
   rw [hfrob],
   apply ring_hom.map_dvd (map_ring_hom (int.cast_ring_hom (zmod p))),
-  exact minpoly_dvd_expand h hprime.1 hdiv
+  exact minpoly_dvd_expand h hdiv
 end
 
 /- Let `P` be the minimal polynomial of a root of unity `μ` and `Q` be the minimal polynomial of