diff --git a/src/algebra/char_p/basic.lean b/src/algebra/char_p/basic.lean
index e367b3d460c11..231939a13f02b 100644
--- a/src/algebra/char_p/basic.lean
+++ b/src/algebra/char_p/basic.lean
@@ -360,6 +360,25 @@ char_ne_zero_of_fintype R (ring_char R)
 
 end
 
+section comm_ring
+
+variables [comm_ring R] [is_reduced R] {R}
+
+@[simp]
+lemma pow_prime_pow_mul_eq_one_iff (p k m : ℕ) [fact p.prime]
+  [char_p R p] (x : R) :
+  x ^ (p ^ k * m) = 1 ↔ x ^ m = 1 :=
+begin
+  induction k with k hk,
+  { rw [pow_zero, one_mul] },
+  { refine ⟨λ h, _, λ h, _⟩,
+    { rw [pow_succ, mul_assoc, pow_mul', ← frobenius_def, ← frobenius_one p] at h,
+      exact hk.1 (frobenius_inj R p h) },
+    { rw [pow_mul', h, one_pow] } }
+end
+
+end comm_ring
+
 section semiring
 open nat
 
diff --git a/src/algebra/ne_zero.lean b/src/algebra/ne_zero.lean
index 14d98c044d322..0520000a99627 100644
--- a/src/algebra/ne_zero.lean
+++ b/src/algebra/ne_zero.lean
@@ -56,6 +56,13 @@ lemma trans [has_zero M] [has_coe R S] [has_coe_t S M] (h : ne_zero ((r : S) : M
 lemma of_map [has_zero R] [has_zero M] [zero_hom_class F R M] (f : F) [ne_zero (f r)] :
   ne_zero r := ⟨λ h, ne (f r) $ by convert map_zero f⟩
 
+lemma nat_of_ne_zero [semiring R] [semiring S] [ring_hom_class F R S] (f : F)
+  [hn : ne_zero (n : S)] : ne_zero (n : R) :=
+begin
+  apply ne_zero.of_map f,
+  simp [hn]
+end
+
 lemma of_injective [has_zero R] [h : ne_zero r] [has_zero M] [zero_hom_class F R M]
   {f : F} (hf : function.injective f) : ne_zero (f r) :=
 ⟨by { rw ←map_zero f, exact hf.ne (ne r) }⟩
diff --git a/src/number_theory/cyclotomic/basic.lean b/src/number_theory/cyclotomic/basic.lean
index df2ab5d3a0fb8..0deb1eff02711 100644
--- a/src/number_theory/cyclotomic/basic.lean
+++ b/src/number_theory/cyclotomic/basic.lean
@@ -8,7 +8,6 @@ import ring_theory.polynomial.cyclotomic.basic
 import number_theory.number_field
 import algebra.char_p.algebra
 import field_theory.galois
-import analysis.complex.polynomial
 
 /-!
 # Cyclotomic extensions
@@ -32,7 +31,8 @@ primitive roots of unity, for all `n ∈ S`.
 ## Main results
 
 * `is_cyclotomic_extension.trans` : if `is_cyclotomic_extension S A B` and
-  `is_cyclotomic_extension T B C`, then `is_cyclotomic_extension (S ∪ T) A C`.
+  `is_cyclotomic_extension T B C`, then `is_cyclotomic_extension (S ∪ T) A C` if
+  `no_zero_smul_divisors B C` and `nontrivial C`.
 * `is_cyclotomic_extension.union_right` : given `is_cyclotomic_extension (S ∪ T) A B`, then
   `is_cyclotomic_extension T (adjoin A { b : B | ∃ a : ℕ+, a ∈ S ∧ b ^ (a : ℕ) = 1 }) B`.
 * `is_cyclotomic_extension.union_right` : given `is_cyclotomic_extension T A B` and `S ⊆ T`, then
@@ -41,16 +41,15 @@ primitive roots of unity, for all `n ∈ S`.
   `B` is a finite `A`-algebra.
 * `is_cyclotomic_extension.number_field` : a finite cyclotomic extension of a number field is a
   number field.
-* `is_cyclotomic_extension.splitting_field_X_pow_sub_one` : if `is_cyclotomic_extension {n} K L`
-  and `ne_zero ((n : ℕ) : K)`, then `L` is the splitting field of `X ^ n - 1`.
-* `is_cyclotomic_extension.splitting_field_cyclotomic` : if `is_cyclotomic_extension {n} K L`
-  and `ne_zero ((n : ℕ) : K)`, then `L` is the splitting field of `cyclotomic n K`.
+* `is_cyclotomic_extension.splitting_field_X_pow_sub_one` : if `is_cyclotomic_extension {n} K L`,
+  then `L` is the splitting field of `X ^ n - 1`.
+* `is_cyclotomic_extension.splitting_field_cyclotomic` : if `is_cyclotomic_extension {n} K L`,
+  then `L` is the splitting field of `cyclotomic n K`.
 
 ## Implementation details
 
 Our definition of `is_cyclotomic_extension` is very general, to allow rings of any characteristic
-and infinite extensions, but it will mainly be used in the case `S = {n}` with `(n : A) ≠ 0` (and
-for integral domains).
+and infinite extensions, but it will mainly be used in the case `S = {n}` and for integral domains.
 All results are in the `is_cyclotomic_extension` namespace.
 Note that some results, for example `is_cyclotomic_extension.trans`,
 `is_cyclotomic_extension.finite`, `is_cyclotomic_extension.number_field`,
@@ -73,10 +72,10 @@ variables [field K] [field L] [algebra K L]
 noncomputable theory
 
 /-- Given an `A`-algebra `B` and `S : set ℕ+`, we define `is_cyclotomic_extension S A B` requiring
-that `cyclotomic a A` has a root in `B` for all `a ∈ S` and that `B` is generated over `A` by the
-roots of `X ^ n - 1`. -/
+that there is a `a`-th primitive root of unity in `B` for all `a ∈ S` and that `B` is generated
+over `A` by the roots of `X ^ n - 1`. -/
 @[mk_iff] class is_cyclotomic_extension : Prop :=
-(exists_root {a : ℕ+} (ha : a ∈ S) : ∃ r : B, aeval r (cyclotomic a A) = 0)
+(exists_prim_root {a : ℕ+} (ha : a ∈ S) : ∃ r : B, is_primitive_root r a)
 (adjoin_roots : ∀ (x : B), x ∈ adjoin A { b : B | ∃ a : ℕ+, a ∈ S ∧ b ^ (a : ℕ) = 1 })
 
 namespace is_cyclotomic_extension
@@ -85,42 +84,38 @@ section basic
 
 /-- A reformulation of `is_cyclotomic_extension` that uses `⊤`. -/
 lemma iff_adjoin_eq_top : is_cyclotomic_extension S A B ↔
- (∀ (a : ℕ+), a ∈ S → ∃ r : B, aeval r (cyclotomic a A) = 0) ∧
+ (∀ (a : ℕ+), a ∈ S → ∃ r : B, is_primitive_root r a) ∧
  (adjoin A { b : B | ∃ a : ℕ+, a ∈ S ∧ b ^ (a : ℕ) = 1 } = ⊤) :=
-⟨λ h, ⟨h.exists_root, algebra.eq_top_iff.2 h.adjoin_roots⟩, λ h, ⟨h.1, algebra.eq_top_iff.1 h.2⟩⟩
+⟨λ h, ⟨h.exists_prim_root, algebra.eq_top_iff.2 h.adjoin_roots⟩,
+  λ h, ⟨h.1, algebra.eq_top_iff.1 h.2⟩⟩
 
 /-- A reformulation of `is_cyclotomic_extension` in the case `S` is a singleton. -/
 lemma iff_singleton : is_cyclotomic_extension {n} A B ↔
- (∃ r : B, aeval r (cyclotomic n A) = 0) ∧
+ (∃ r : B, is_primitive_root r n) ∧
  (∀ x, x ∈ adjoin A { b : B | b ^ (n : ℕ) = 1 }) :=
 by simp [is_cyclotomic_extension_iff]
 
-/-- If `is_cyclotomic_extension ∅ A B`, then `A = B`. -/
+/-- If `is_cyclotomic_extension ∅ A B`, then the image of `A` in `B` equals `B`. -/
 lemma empty [h : is_cyclotomic_extension ∅ A B] : (⊥ : subalgebra A B) = ⊤ :=
 by simpa [algebra.eq_top_iff, is_cyclotomic_extension_iff] using h
 
-/-- If `is_cyclotomic_extension {1} A B`, then `A = B`. -/
+/-- If `is_cyclotomic_extension {1} A B`, then the image of `A` in `B` equals `B`. -/
 lemma singleton_one [h : is_cyclotomic_extension {1} A B] : (⊥ : subalgebra A B) = ⊤ :=
 algebra.eq_top_iff.2 (λ x, by simpa [adjoin_singleton_one]
   using ((is_cyclotomic_extension_iff _ _ _).1 h).2 x)
 
 /-- Transitivity of cyclotomic extensions. -/
-lemma trans (C : Type w) [comm_ring C] [algebra A C] [algebra B C]
+lemma trans (C : Type w) [comm_ring C] [nontrivial C] [algebra A C] [algebra B C]
   [is_scalar_tower A B C] [hS : is_cyclotomic_extension S A B]
-  [hT : is_cyclotomic_extension T B C] : is_cyclotomic_extension (S ∪ T) A C :=
+  [hT : is_cyclotomic_extension T B C] [no_zero_smul_divisors B C] :
+  is_cyclotomic_extension (S ∪ T) A C :=
 begin
   refine ⟨λ n hn, _, λ x, _⟩,
   { cases hn,
     { obtain ⟨b, hb⟩ := ((is_cyclotomic_extension_iff _ _ _).1 hS).1 hn,
       refine ⟨algebra_map B C b, _⟩,
-      replace hb := congr_arg (algebra_map B C) hb,
-      rw [aeval_def, eval₂_eq_eval_map, map_cyclotomic, ring_hom.map_zero, ← eval₂_at_apply,
-        eval₂_eq_eval_map, map_cyclotomic] at hb,
-      rwa [aeval_def, eval₂_eq_eval_map, map_cyclotomic] },
-    { obtain ⟨c, hc⟩ := ((is_cyclotomic_extension_iff _ _ _).1 hT).1 hn,
-      refine ⟨c, _⟩,
-      rw [aeval_def, eval₂_eq_eval_map, map_cyclotomic] at hc,
-      rwa [aeval_def, eval₂_eq_eval_map, map_cyclotomic] } },
+      exact hb.map_of_injective (no_zero_smul_divisors.algebra_map_injective B C) },
+    { exact ((is_cyclotomic_extension_iff _ _ _).1 hT).1 hn } },
   { refine adjoin_induction (((is_cyclotomic_extension_iff _ _ _).1 hT).2 x) (λ c ⟨n, hn⟩,
       subset_adjoin ⟨n, or.inr hn.1, hn.2⟩) (λ b, _) (λ x y hx hy, subalgebra.add_mem _ hx hy)
       (λ x y hx hy, subalgebra.mul_mem _ hx hy),
@@ -133,6 +128,22 @@ begin
       exact ⟨n, ⟨mem_union_left T hn.1, by rw [← h₁, ← alg_hom.map_pow, hn.2, alg_hom.map_one]⟩⟩ } }
 end
 
+@[nontriviality] lemma subsingleton_iff [subsingleton B] :
+  is_cyclotomic_extension S A B ↔ S = {} ∨ S = {1} :=
+begin
+  split,
+  { rintro ⟨hprim, -⟩,
+    rw ←subset_singleton_iff_eq,
+    intros t ht,
+    obtain ⟨ζ, hζ⟩ := hprim ht,
+    rw [mem_singleton_iff, ←pnat.coe_eq_one_iff],
+    exact_mod_cast hζ.unique (is_primitive_root.of_subsingleton ζ) },
+  { rintro (rfl|rfl),
+    { refine ⟨λ _ h, h.elim, λ x, by convert subalgebra.zero_mem _⟩ },
+    { rw iff_singleton,
+      refine ⟨⟨0, is_primitive_root.of_subsingleton 0⟩, λ x, by convert subalgebra.zero_mem _⟩ } }
+end
+
 /-- If `B` is a cyclotomic extension of `A` given by roots of unity of order in `S ∪ T`, then `B`
 is a cyclotomic extension of `adjoin A { b : B | ∃ a : ℕ+, a ∈ S ∧ b ^ (a : ℕ) = 1 } ` given by
 roots of unity of order in `T`. -/
@@ -150,14 +161,9 @@ begin
       { exact ⟨n, or.inl hn.1, hn.2⟩ },
       { exact ⟨n, or.inr hn.1, hn.2⟩ } } },
 
-  refine ⟨λ n hn, _, λ b, _⟩,
-  { obtain ⟨b, hb⟩ := ((is_cyclotomic_extension_iff _ _ _).1 h).1 (mem_union_right S hn),
-    refine ⟨b, _⟩,
-    rw [aeval_def, eval₂_eq_eval_map, map_cyclotomic] at hb,
-    rwa [aeval_def, eval₂_eq_eval_map, map_cyclotomic] },
-  { replace h := ((is_cyclotomic_extension_iff _ _ _).1 h).2 b,
-    rwa [this, adjoin_union_eq_adjoin_adjoin,
-      subalgebra.mem_restrict_scalars] at h }
+  refine ⟨λ n hn, ((is_cyclotomic_extension_iff _ _ _).1 h).1 (mem_union_right S hn), λ b, _⟩,
+  replace h := ((is_cyclotomic_extension_iff _ _ _).1 h).2 b,
+  rwa [this, adjoin_union_eq_adjoin_adjoin, subalgebra.mem_restrict_scalars] at h
 end
 
 /-- If `B` is a cyclotomic extension of `A` given by roots of unity of order in `T` and `S ⊆ T`,
@@ -168,15 +174,25 @@ lemma union_left [h : is_cyclotomic_extension T A B] (hS : S ⊆ T) :
 begin
   refine ⟨λ n hn, _, λ b, _⟩,
   { obtain ⟨b, hb⟩ := ((is_cyclotomic_extension_iff _ _ _).1 h).1 (hS hn),
-    refine ⟨⟨b, subset_adjoin ⟨n, hn, _⟩⟩, _⟩,
-    { rw [aeval_def, eval₂_eq_eval_map, map_cyclotomic, ← is_root.def] at hb,
-      suffices : (X ^ (n : ℕ) - 1).is_root b,
-      { simpa [sub_eq_zero] using this },
-      exact hb.dvd (cyclotomic.dvd_X_pow_sub_one _ _) },
-      rwa [← subalgebra.coe_eq_zero, aeval_subalgebra_coe, subtype.coe_mk] },
+    refine ⟨⟨b, subset_adjoin ⟨n, hn, hb.pow_eq_one⟩⟩, _⟩,
+    rwa [← is_primitive_root.coe_submonoid_class_iff, subtype.coe_mk] },
   { convert mem_top,
     rw [← adjoin_adjoin_coe_preimage, preimage_set_of_eq],
-    norm_cast, }
+    norm_cast }
+end
+
+@[protected]
+lemma ne_zero [h : is_cyclotomic_extension {n} A B] [is_domain B] : ne_zero ((n : ℕ) : B) :=
+begin
+  obtain ⟨⟨r, hr⟩, -⟩ := (iff_singleton n A B).1 h,
+  exact hr.ne_zero'
+end
+
+@[protected]
+lemma ne_zero' [is_cyclotomic_extension {n} A B] [is_domain B] : ne_zero ((n : ℕ) : A) :=
+begin
+  apply ne_zero.nat_of_ne_zero (algebra_map A B),
+  exact ne_zero n A B,
 end
 
 end basic
@@ -245,7 +261,7 @@ section
 variables {A B}
 
 lemma adjoin_roots_cyclotomic_eq_adjoin_nth_roots [decidable_eq B] [is_domain B] {ζ : B}
-  (hζ : is_primitive_root ζ n) :
+  {n : ℕ+} (hζ : is_primitive_root ζ n) :
   adjoin A ↑((map (algebra_map A B) (cyclotomic n A)).roots.to_finset) =
   adjoin A {b : B | ∃ (a : ℕ+), a ∈ ({n} : set ℕ+) ∧ b ^ (a : ℕ) = 1} :=
 begin
@@ -263,8 +279,8 @@ begin
     exact hζ.is_root_cyclotomic n.pos }
 end
 
-lemma adjoin_roots_cyclotomic_eq_adjoin_root_cyclotomic [decidable_eq B] [is_domain B]
-  (ζ : B) (hζ : is_primitive_root ζ n) :
+lemma adjoin_roots_cyclotomic_eq_adjoin_root_cyclotomic {n : ℕ+} [decidable_eq B] [is_domain B]
+  {ζ : B} (hζ : is_primitive_root ζ n) :
   adjoin A (((map (algebra_map A B) (cyclotomic n A)).roots.to_finset) : set B) = adjoin A ({ζ}) :=
 begin
   refine le_antisymm (adjoin_le (λ x hx, _)) (adjoin_mono (λ x hx, _)),
@@ -280,26 +296,24 @@ begin
                 mem_roots (cyclotomic_ne_zero n B)] using hζ.is_root_cyclotomic n.pos }
 end
 
-lemma adjoin_primitive_root_eq_top [is_domain B] [h : is_cyclotomic_extension {n} A B]
-  (ζ : B) (hζ : is_primitive_root ζ n) : adjoin A ({ζ} : set B) = ⊤ :=
+lemma adjoin_primitive_root_eq_top {n : ℕ+} [is_domain B] [h : is_cyclotomic_extension {n} A B]
+  {ζ : B} (hζ : is_primitive_root ζ n) : adjoin A ({ζ} : set B) = ⊤ :=
 begin
   classical,
-  rw ←adjoin_roots_cyclotomic_eq_adjoin_root_cyclotomic n ζ hζ,
-  rw adjoin_roots_cyclotomic_eq_adjoin_nth_roots n hζ,
+  rw ←adjoin_roots_cyclotomic_eq_adjoin_root_cyclotomic hζ,
+  rw adjoin_roots_cyclotomic_eq_adjoin_nth_roots hζ,
   exact ((iff_adjoin_eq_top {n} A B).mp h).2,
 end
 
 variable (A)
 
-lemma _root_.is_primitive_root.adjoin_is_cyclotomic_extension [is_domain B] {ζ : B} {n : ℕ+}
+lemma _root_.is_primitive_root.adjoin_is_cyclotomic_extension {ζ : B} {n : ℕ+}
   (h : is_primitive_root ζ n) : is_cyclotomic_extension {n} A (adjoin A ({ζ} : set B)) :=
-{ exists_root := λ i hi,
+{ exists_prim_root := λ i hi,
   begin
     rw [set.mem_singleton_iff] at hi,
     refine ⟨⟨ζ, subset_adjoin $ set.mem_singleton ζ⟩, _⟩,
-    replace h := h.is_root_cyclotomic n.pos,
-    rw [is_root.def, ← map_cyclotomic _ (algebra_map A B), eval_map, ← aeval_def, ← hi] at h,
-    rwa [← subalgebra.coe_eq_zero, aeval_subalgebra_coe, subtype.coe_mk]
+    rwa [← is_primitive_root.coe_submonoid_class_iff, subtype.coe_mk, hi],
   end,
   adjoin_roots := λ x,
   begin
@@ -318,18 +332,16 @@ end
 
 section field
 
-variable [ne_zero ((n : ℕ) : K)]
+variables {n S}
 
-/-- A cyclotomic extension splits `X ^ n - 1` if `n ∈ S` and `ne_zero (n : K)`.-/
+/-- A cyclotomic extension splits `X ^ n - 1` if `n ∈ S`.-/
 lemma splits_X_pow_sub_one [H : is_cyclotomic_extension S K L] (hS : n ∈ S) :
   splits (algebra_map K L) (X ^ (n : ℕ) - 1) :=
 begin
   rw [← splits_id_iff_splits, polynomial.map_sub, polynomial.map_one,
       polynomial.map_pow, polynomial.map_X],
   obtain ⟨z, hz⟩ := ((is_cyclotomic_extension_iff _ _ _).1 H).1 hS,
-  rw [aeval_def, eval₂_eq_eval_map, map_cyclotomic] at hz,
-  haveI := ne_zero.of_no_zero_smul_divisors K L n,
-  exact X_pow_sub_one_splits (is_root_cyclotomic_iff.1 hz),
+  exact X_pow_sub_one_splits hz,
 end
 
 /-- A cyclotomic extension splits `cyclotomic n K` if `n ∈ S` and `ne_zero (n : K)`.-/
@@ -337,19 +349,20 @@ lemma splits_cyclotomic [is_cyclotomic_extension S K L] (hS : n ∈ S) :
   splits (algebra_map K L) (cyclotomic n K) :=
 begin
   refine splits_of_splits_of_dvd _ (X_pow_sub_C_ne_zero n.pos _)
-    (splits_X_pow_sub_one n S K L hS) _,
+    (splits_X_pow_sub_one K L hS) _,
   use (∏ (i : ℕ) in (n : ℕ).proper_divisors, polynomial.cyclotomic i K),
   rw [(eq_cyclotomic_iff n.pos _).1 rfl, ring_hom.map_one],
 end
 
+variables (n S)
+
 section singleton
 
 variables [is_cyclotomic_extension {n} K L]
 
-/-- If `is_cyclotomic_extension {n} K L` and `ne_zero ((n : ℕ) : K)`, then `L` is the splitting
-field of `X ^ n - 1`. -/
+/-- If `is_cyclotomic_extension {n} K L`, then `L` is the splitting field of `X ^ n - 1`. -/
 lemma splitting_field_X_pow_sub_one : is_splitting_field K L (X ^ (n : ℕ) - 1) :=
-{ splits := splits_X_pow_sub_one n {n} K L (mem_singleton n),
+{ splits := splits_X_pow_sub_one K L (mem_singleton n),
   adjoin_roots :=
   begin
     rw [← ((iff_adjoin_eq_top {n} K L).1 infer_instance).2],
@@ -368,24 +381,20 @@ include n
 lemma is_galois : is_galois K L :=
 begin
   letI := splitting_field_X_pow_sub_one n K L,
-  exact is_galois.of_separable_splitting_field (X_pow_sub_one_separable_iff.2
-    (ne_zero.ne _ : ((n : ℕ) : K) ≠ 0)),
+  exact is_galois.of_separable_splitting_field (X_pow_sub_one_separable_iff.2 ((ne_zero' n K L).1))
 end
 
 localized "attribute [instance] is_cyclotomic_extension.is_galois" in cyclotomic
 
-/-- If `is_cyclotomic_extension {n} K L` and `ne_zero ((n : ℕ) : K)`, then `L` is the splitting
-field of `cyclotomic n K`. -/
+/-- If `is_cyclotomic_extension {n} K L`, then `L` is the splitting field of `cyclotomic n K`. -/
 lemma splitting_field_cyclotomic : is_splitting_field K L (cyclotomic n K) :=
-{ splits := splits_cyclotomic n {n} K L (mem_singleton n),
+{ splits := splits_cyclotomic K L (mem_singleton n),
   adjoin_roots :=
   begin
     rw [← ((iff_adjoin_eq_top {n} K L).1 infer_instance).2],
     letI := classical.dec_eq L,
-    obtain ⟨ζ, hζ⟩ := @is_cyclotomic_extension.exists_root {n} K L _ _ _ _ _ (mem_singleton n),
-    haveI : ne_zero ((n : ℕ) : L) := ne_zero.nat_of_injective (algebra_map K L).injective,
-    rw [aeval_def, eval₂_eq_eval_map, map_cyclotomic, ← is_root.def, is_root_cyclotomic_iff] at hζ,
-    refine adjoin_roots_cyclotomic_eq_adjoin_nth_roots n hζ
+    obtain ⟨ζ, hζ⟩ := @is_cyclotomic_extension.exists_prim_root {n} K L _ _ _ _ _ (mem_singleton n),
+    exact adjoin_roots_cyclotomic_eq_adjoin_nth_roots hζ
   end }
 
 localized "attribute [instance] is_cyclotomic_extension.splitting_field_cyclotomic" in cyclotomic
@@ -406,13 +415,20 @@ def cyclotomic_field : Type w := (cyclotomic n K).splitting_field
 
 namespace cyclotomic_field
 
+instance [char_zero K] : char_zero (cyclotomic_field n K) :=
+char_zero_of_injective_algebra_map ((algebra_map K _).injective)
+
 instance is_cyclotomic_extension [ne_zero ((n : ℕ) : K)] :
   is_cyclotomic_extension {n} K (cyclotomic_field n K) :=
-{ exists_root := λ a han,
+{ exists_prim_root := λ a han,
   begin
     rw mem_singleton_iff at han,
     subst a,
-    exact exists_root_of_splits _ (splitting_field.splits _) (degree_cyclotomic_pos n K (n.pos)).ne'
+    obtain ⟨r, hr⟩ := exists_root_of_splits (algebra_map K (cyclotomic_field n K))
+      (splitting_field.splits _) (degree_cyclotomic_pos n K (n.pos)).ne',
+    refine ⟨r, _⟩,
+    haveI := ne_zero.of_no_zero_smul_divisors K (cyclotomic_field n K) n,
+    rwa [← eval_map, ← is_root.def, map_cyclotomic, is_root_cyclotomic_iff] at hr
   end,
   adjoin_roots :=
   begin
@@ -423,7 +439,7 @@ instance is_cyclotomic_extension [ne_zero ((n : ℕ) : K)] :
     haveI : ne_zero ((n : ℕ) : (cyclotomic_field n K)) :=
       ne_zero.nat_of_injective (algebra_map K _).injective,
     rw [eval₂_eq_eval_map, map_cyclotomic, ← is_root.def, is_root_cyclotomic_iff] at hζ,
-    exact is_cyclotomic_extension.adjoin_roots_cyclotomic_eq_adjoin_nth_roots n hζ,
+    exact is_cyclotomic_extension.adjoin_roots_cyclotomic_eq_adjoin_nth_roots hζ,
   end }
 
 end cyclotomic_field
@@ -482,22 +498,19 @@ is_scalar_tower.subalgebra' _ _ _ _
 
 instance is_cyclotomic_extension [ne_zero ((n : ℕ) : A)] :
   is_cyclotomic_extension {n} A (cyclotomic_ring n A K) :=
-{ exists_root := λ a han,
+{ exists_prim_root := λ a han,
   begin
     rw mem_singleton_iff at han,
     subst a,
     haveI := ne_zero.of_no_zero_smul_divisors A K n,
-    haveI := ne_zero.of_no_zero_smul_divisors A (cyclotomic_ring n A K) n,
     haveI := ne_zero.of_no_zero_smul_divisors A (cyclotomic_field n K) n,
-    obtain ⟨μ, hμ⟩ := let h := (cyclotomic_field.is_cyclotomic_extension n K).exists_root
+    obtain ⟨μ, hμ⟩ := let h := (cyclotomic_field.is_cyclotomic_extension n K).exists_prim_root
                       in h $ mem_singleton n,
     refine ⟨⟨μ, subset_adjoin _⟩, _⟩,
     { apply (is_root_of_unity_iff n.pos (cyclotomic_field n K)).mpr,
       refine ⟨n, nat.mem_divisors_self _ n.ne_zero, _⟩,
-      rwa [aeval_def, eval₂_eq_eval_map, map_cyclotomic] at hμ },
-    simp_rw [aeval_def, eval₂_eq_eval_map,
-      map_cyclotomic, ←is_root.def, is_root_cyclotomic_iff] at hμ ⊢,
-    rwa ←is_primitive_root.map_iff_of_injective (adjoin_algebra_injective n A K)
+      rwa [← is_root_cyclotomic_iff] at hμ },
+    { rwa [← is_primitive_root.coe_submonoid_class_iff, subtype.coe_mk] }
   end,
   adjoin_roots := λ x,
   begin
@@ -553,8 +566,8 @@ lemma eq_adjoin_primitive_root {μ : (cyclotomic_field n K)} (h : is_primitive_r
   cyclotomic_ring n A K = adjoin A ({μ} : set ((cyclotomic_field n K))) :=
 begin
   letI := classical.prop_decidable,
-  rw [←is_cyclotomic_extension.adjoin_roots_cyclotomic_eq_adjoin_root_cyclotomic n μ h,
-      is_cyclotomic_extension.adjoin_roots_cyclotomic_eq_adjoin_nth_roots n h],
+  rw [←is_cyclotomic_extension.adjoin_roots_cyclotomic_eq_adjoin_root_cyclotomic h,
+      is_cyclotomic_extension.adjoin_roots_cyclotomic_eq_adjoin_nth_roots h],
   simp [cyclotomic_ring]
 end
 
@@ -564,10 +577,24 @@ end cyclotomic_ring
 
 end is_domain
 
-/-- Algebraically closed fields are cyclotomic extensions over themselves. -/
-lemma is_alg_closed.is_cyclotomic_extension (K) [field K] [is_alg_closed K] (S) :
+section is_alg_closed
+
+variables [is_alg_closed K]
+
+/-- Algebraically closed fields are `S`-cyclotomic extensions over themselves if
+`ne_zero ((a : ℕ) : K))` for all `a ∈ S`. -/
+lemma is_alg_closed.is_cyclotomic_extension (h : ∀ a ∈ S, ne_zero ((a : ℕ) : K)) :
   is_cyclotomic_extension S K K :=
-⟨λ a _, is_alg_closed.exists_aeval_eq_zero _ _ (degree_cyclotomic_pos _ _ a.pos).ne',
- algebra.eq_top_iff.mp $ subsingleton.elim _ _ ⟩
+begin
+  refine ⟨λ a ha, _,  algebra.eq_top_iff.mp $ subsingleton.elim _ _ ⟩,
+  obtain ⟨r, hr⟩ := is_alg_closed.exists_aeval_eq_zero K _ (degree_cyclotomic_pos a K a.pos).ne',
+  refine ⟨r, _⟩,
+  haveI := h a ha,
+  rwa [coe_aeval_eq_eval, ← is_root.def, is_root_cyclotomic_iff] at hr,
+end
+
+instance is_alg_closed_of_char_zero.is_cyclotomic_extension [char_zero K] :
+  ∀ S, is_cyclotomic_extension S K K :=
+λ S, is_alg_closed.is_cyclotomic_extension S K (λ a ha, infer_instance)
 
-instance : ∀ S, is_cyclotomic_extension S ℂ ℂ := is_alg_closed.is_cyclotomic_extension ℂ
+end is_alg_closed
diff --git a/src/number_theory/cyclotomic/discriminant.lean b/src/number_theory/cyclotomic/discriminant.lean
index 64650d5b5da33..c9d29d4e626a7 100644
--- a/src/number_theory/cyclotomic/discriminant.lean
+++ b/src/number_theory/cyclotomic/discriminant.lean
@@ -35,13 +35,14 @@ discriminant of the power basis given by `ζ - 1`. -/
 lemma discr_zeta_eq_discr_zeta_sub_one (hζ : is_primitive_root ζ n) :
   discr ℚ (hζ.power_basis ℚ).basis = discr ℚ (hζ.sub_one_power_basis ℚ).basis :=
 begin
+  haveI : number_field K := number_field.mk,
   have H₁ : (aeval (hζ.power_basis ℚ).gen) (X - 1 : ℤ[X]) = (hζ.sub_one_power_basis ℚ).gen :=
     by simp,
   have H₂ : (aeval (hζ.sub_one_power_basis ℚ).gen) (X + 1 : ℤ[X]) = (hζ.power_basis ℚ).gen :=
     by simp,
   refine discr_eq_discr_of_to_matrix_coeff_is_integral _
-    (λ i j, to_matrix_is_integral H₁ _  _ _ _)
-    (λ i j, to_matrix_is_integral H₂ _  _ _ _),
+    (λ 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) },
   { exact is_integral_sub (hζ.is_integral n.pos) is_integral_one },
@@ -60,16 +61,12 @@ variables [algebra K L]
 `hζ.power_basis K` is `(-1) ^ ((p ^ (k + 1).totient) / 2) * p ^ (p ^ k * ((p - 1) * (k + 1) - 1))`
 if `irreducible (cyclotomic (p ^ (k + 1)) K))`, and `p ^ (k + 1) ≠ 2`. -/
 lemma discr_prime_pow_ne_two [is_cyclotomic_extension {p ^ (k + 1)} K L] [hp : fact (p : ℕ).prime]
-  [ne_zero ((p : ℕ) : K)] (hζ : is_primitive_root ζ ↑(p ^ (k + 1)))
-  (hirr : irreducible (cyclotomic (↑(p ^ (k + 1)) : ℕ) K))
+  (hζ : is_primitive_root ζ ↑(p ^ (k + 1))) (hirr : irreducible (cyclotomic (↑(p ^ (k + 1)) : ℕ) K))
   (hk : p ^ (k + 1) ≠ 2) :
   discr K (hζ.power_basis K).basis =
   (-1) ^ (((p ^ (k + 1) : ℕ).totient) / 2) * p ^ ((p : ℕ) ^ k * ((p - 1) * (k + 1) - 1)) :=
 begin
-  haveI : ne_zero ((↑(p ^ (k + 1)) : ℕ) : K),
-  { refine ⟨λ hzero, _⟩,
-    rw [pnat.pow_coe] at hzero,
-    simpa [ne_zero.ne ((p : ℕ) : K)] using hzero },
+  haveI hne := is_cyclotomic_extension.ne_zero' (p ^ (k + 1)) K L,
   have hp2 : p = 2 → 1 ≤ k,
   { intro hp,
     refine one_le_iff_ne_zero.2 (λ h, _),
@@ -128,7 +125,7 @@ begin
       { simpa only [← pnat.pow_coe, H, mul_comm _ (k + 1)] },
       { replace h := pow_eq_zero h,
         rw [coe_coe] at h,
-        exact ne_zero.ne _ h } },
+        simpa using hne.1 } },
     all_goals { apply_instance } },
   all_goals { apply_instance }
 end
@@ -137,8 +134,8 @@ end
 `hζ.power_basis K` is `(-1) ^ (p ^ k * (p - 1) / 2) * p ^ (p ^ k * ((p - 1) * (k + 1) - 1))`
 if `irreducible (cyclotomic (p ^ (k + 1)) K))`, and `p ^ (k + 1) ≠ 2`. -/
 lemma discr_prime_pow_ne_two' [is_cyclotomic_extension {p ^ (k + 1)} K L] [hp : fact (p : ℕ).prime]
-  [ne_zero ((p : ℕ) : K)] (hζ : is_primitive_root ζ ↑(p ^ (k + 1)))
-  (hirr : irreducible (cyclotomic (↑(p ^ (k + 1)) : ℕ) K)) (hk : p ^ (k + 1) ≠ 2) :
+  (hζ : is_primitive_root ζ ↑(p ^ (k + 1))) (hirr : irreducible (cyclotomic (↑(p ^ (k + 1)) : ℕ) K))
+  (hk : p ^ (k + 1) ≠ 2) :
   discr K (hζ.power_basis K).basis =
   (-1) ^ (((p : ℕ) ^ k  * (p - 1)) / 2) * p ^ ((p : ℕ) ^ k * ((p - 1) * (k + 1) - 1)) :=
 by simpa [totient_prime_pow hp.out (succ_pos k)] using discr_prime_pow_ne_two hζ hirr hk
@@ -149,14 +146,12 @@ if `irreducible (cyclotomic (p ^ k) K))`. Beware that in the cases `p ^ k = 1` a
 the formula uses `1 / 2 = 0` and `0 - 1 = 0`. It is useful only to have a uniform result.
 See also `is_cyclotomic_extension.discr_prime_pow_eq_unit_mul_pow`. -/
 lemma discr_prime_pow [hcycl : is_cyclotomic_extension {p ^ k} K L] [hp : fact (p : ℕ).prime]
-  [ne_zero ((p : ℕ) : K)] (hζ : is_primitive_root ζ ↑(p ^ k))
-  (hirr : irreducible (cyclotomic (↑(p ^ k) : ℕ) K)) :
+  (hζ : is_primitive_root ζ ↑(p ^ k)) (hirr : irreducible (cyclotomic (↑(p ^ k) : ℕ) K)) :
   discr K (hζ.power_basis K).basis =
   (-1) ^ (((p ^ k : ℕ).totient) / 2) * p ^ ((p : ℕ) ^ (k - 1) * ((p - 1) * k - 1)) :=
 begin
   unfreezingI { cases k },
-  { haveI : ne_zero ((↑(p ^ 0) : ℕ) : K) := ⟨by simp⟩,
-    simp only [coe_basis, pow_zero, power_basis_gen, totient_one, mul_zero, mul_one, show 1 / 2 = 0,
+  { simp only [coe_basis, pow_zero, power_basis_gen, totient_one, mul_zero, mul_one, show 1 / 2 = 0,
       by refl, discr, trace_matrix],
     have hζone : ζ = 1 := by simpa using hζ,
     rw [hζ.power_basis_dim _, hζone, ← (algebra_map K L).map_one,
@@ -167,11 +162,7 @@ begin
     { apply_instance },
     { exact hcycl } },
   { by_cases hk : p ^ (k + 1) = 2,
-    { haveI : ne_zero ((↑(p ^ (k + 1)) : ℕ) : K),
-      { refine ⟨λ hzero, _⟩,
-        rw [pnat.pow_coe] at hzero,
-        simpa [ne_zero.ne ((p : ℕ) : K)] using hzero },
-      have hp : p = 2,
+    { have hp : p = 2,
       { rw [← pnat.coe_inj, pnat.coe_bit0, pnat.one_coe, pnat.pow_coe, ← pow_one 2] at hk,
       replace hk := eq_of_prime_pow_eq (prime_iff.1 hp.out) (prime_iff.1 nat.prime_two)
         (succ_pos _) hk,
@@ -199,7 +190,7 @@ end
 `n : ℕ` such that the discriminant of `hζ.power_basis K` is `u * p ^ n`. Often this is enough and
 less cumbersome to use than `is_cyclotomic_extension.discr_prime_pow`. -/
 lemma discr_prime_pow_eq_unit_mul_pow [is_cyclotomic_extension {p ^ k} K L]
-  [hp : fact (p : ℕ).prime] [ne_zero ((p : ℕ) : K)] (hζ : is_primitive_root ζ ↑(p ^ k))
+  [hp : fact (p : ℕ).prime] (hζ : is_primitive_root ζ ↑(p ^ k))
   (hirr : irreducible (cyclotomic (↑(p ^ k) : ℕ) K)) :
   ∃ (u : ℤˣ) (n : ℕ), discr K (hζ.power_basis K).basis = u * p ^ n :=
 begin
@@ -214,8 +205,7 @@ end
 `discr K (hζ.power_basis K).basis = (-1) ^ ((p - 1) / 2) * p ^ (p - 2)` if
 `irreducible (cyclotomic p K)`. -/
 lemma discr_odd_prime [is_cyclotomic_extension {p} K L] [hp : fact (p : ℕ).prime]
-  [ne_zero ((p : ℕ) : K)] (hζ : is_primitive_root ζ p) (hirr : irreducible (cyclotomic p K))
-  (hodd : p ≠ 2) :
+  (hζ : is_primitive_root ζ p) (hirr : irreducible (cyclotomic p K)) (hodd : p ≠ 2) :
   discr K (hζ.power_basis K).basis = (-1) ^ (((p : ℕ) - 1) / 2) * p ^ ((p : ℕ) - 2) :=
 begin
   haveI : is_cyclotomic_extension {p ^ (0 + 1)} K L,
diff --git a/src/number_theory/cyclotomic/gal.lean b/src/number_theory/cyclotomic/gal.lean
index 6bda15559e2f3..d4f9dbd21fcfc 100644
--- a/src/number_theory/cyclotomic/gal.lean
+++ b/src/number_theory/cyclotomic/gal.lean
@@ -16,10 +16,9 @@ it is always a subgroup, and if the `n`th cyclotomic polynomial is irreducible,
 ## Main results
 
 * `is_primitive_root.aut_to_pow_injective`: `is_primitive_root.aut_to_pow` is injective
-  in the case that it's considered over a cyclotomic field extension, where `n` does not divide
-  the characteristic of K.
-* `is_cyclotomic_extension.aut_equiv_pow`: If, additionally, the `n`th cyclotomic polynomial is
-  irreducible in K, then `aut_to_pow` is a `mul_equiv` (for example, in ℚ and certain 𝔽ₚ).
+  in the case that it's considered over a cyclotomic field extension.
+* `is_cyclotomic_extension.aut_equiv_pow`: If the `n`th cyclotomic polynomial is irreducible
+  in `K`, then `aut_to_pow` is a `mul_equiv` (for example, in `ℚ` and certain `𝔽ₚ`).
 * `gal_X_pow_equiv_units_zmod`, `gal_cyclotomic_equiv_units_zmod`: Repackage `aut_equiv_pow` in
   terms of `polynomial.gal`.
 * `is_cyclotomic_extension.aut.comm_group`: Cyclotomic extensions are abelian.
@@ -43,14 +42,14 @@ local attribute [instance] pnat.fact_pos
 variables {n : ℕ+} (K : Type*) [field K] {L : Type*} [field L] {μ : L} (hμ : is_primitive_root μ n)
           [algebra K L] [is_cyclotomic_extension {n} K L]
 
-open polynomial ne_zero is_cyclotomic_extension
+open polynomial is_cyclotomic_extension
 
 open_locale cyclotomic
 
 namespace is_primitive_root
 
 /-- `is_primitive_root.aut_to_pow` is injective in the case that it's considered over a cyclotomic
-field extension, where `n` does not divide the characteristic of K. -/
+field extension. -/
 lemma aut_to_pow_injective : function.injective $ hμ.aut_to_pow K :=
 begin
   intros f g hfg,
@@ -80,9 +79,8 @@ end is_primitive_root
 namespace is_cyclotomic_extension
 
 /-- Cyclotomic extensions are abelian. -/
-noncomputable def aut.comm_group [ne_zero ((n : ℕ) : K)] : comm_group (L ≃ₐ[K] L) :=
-let _ := of_no_zero_smul_divisors K L n in by exactI
-((zeta_primitive_root n K L).aut_to_pow_injective K).comm_group _
+noncomputable def aut.comm_group : comm_group (L ≃ₐ[K] L) :=
+((zeta_spec n K L).aut_to_pow_injective K).comm_group _
   (map_one _) (map_mul _) (map_inv _) (map_div _) (map_pow _) (map_zpow _)
 
 variables (h : irreducible (cyclotomic n K)) {K} (L)
@@ -91,17 +89,16 @@ include h
 
 /-- The `mul_equiv` that takes an automorphism `f` to the element `k : (zmod n)ˣ` such that
   `f μ = μ ^ k`. A stronger version of `is_primitive_root.aut_to_pow`. -/
-@[simps] noncomputable def aut_equiv_pow [ne_zero ((n : ℕ) : K)] : (L ≃ₐ[K] L) ≃* (zmod n)ˣ :=
-let hn := of_no_zero_smul_divisors K L n in
-by exactI
-let hζ := zeta_primitive_root n K L,
+@[simps] noncomputable def aut_equiv_pow : (L ≃ₐ[K] L) ≃* (zmod n)ˣ :=
+let hζ := zeta_spec n K L,
     hμ := λ t, hζ.pow_of_coprime _ (zmod.val_coe_unit_coprime t) in
 { inv_fun := λ t, (hζ.power_basis K).equiv_of_minpoly ((hμ t).power_basis K)
   begin
+    haveI := is_cyclotomic_extension.ne_zero' n K L,
     simp only [is_primitive_root.power_basis_gen],
     have hr := is_primitive_root.minpoly_eq_cyclotomic_of_irreducible
-               ((zeta_primitive_root n K L).pow_of_coprime _ (zmod.val_coe_unit_coprime t)) h,
-    exact ((zeta_primitive_root n K L).minpoly_eq_cyclotomic_of_irreducible h).symm.trans hr
+               ((zeta_spec n K L).pow_of_coprime _ (zmod.val_coe_unit_coprime t)) h,
+    exact ((zeta_spec n K L).minpoly_eq_cyclotomic_of_irreducible h).symm.trans hr
   end,
   left_inv := λ f, begin
     simp only [monoid_hom.to_fun_eq_coe],
@@ -123,24 +120,23 @@ let hζ := zeta_primitive_root n K L,
     simp only [←coe_coe, ←roots_of_unity.coe_pow] at key,
     replace key := roots_of_unity.coe_injective key,
     rw [pow_eq_pow_iff_modeq, ←order_of_subgroup, ←order_of_units, hζ.coe_to_roots_of_unity_coe,
-        ←(zeta_primitive_root n K L).eq_order_of, ←zmod.eq_iff_modeq_nat] at key,
+        ←(zeta_spec n K L).eq_order_of, ←zmod.eq_iff_modeq_nat] at key,
     simp only [zmod.nat_cast_val, zmod.cast_id', id.def] at key,
     exact units.ext key
   end,
-  .. (zeta_primitive_root n K L).aut_to_pow K }
+  .. (zeta_spec n K L).aut_to_pow K }
 
 include hμ
 
 variables {L}
 
 /-- Maps `μ` to the `alg_equiv` that sends `is_cyclotomic_extension.zeta` to `μ`. -/
-noncomputable def from_zeta_aut [ne_zero ((n : ℕ) : K)] : L ≃ₐ[K] L :=
-have _ := of_no_zero_smul_divisors K L n, by exactI
-let hζ := (zeta_primitive_root n K L).eq_pow_of_pow_eq_one hμ.pow_eq_one n.pos in
+noncomputable def from_zeta_aut : L ≃ₐ[K] L :=
+let hζ := (zeta_spec n K L).eq_pow_of_pow_eq_one hμ.pow_eq_one n.pos in
 (aut_equiv_pow L h).symm $ zmod.unit_of_coprime hζ.some $
-((zeta_primitive_root n K L).pow_iff_coprime n.pos hζ.some).mp $ hζ.some_spec.some_spec.symm ▸ hμ
+((zeta_spec n K L).pow_iff_coprime n.pos hζ.some).mp $ hζ.some_spec.some_spec.symm ▸ hμ
 
-lemma from_zeta_aut_spec [ne_zero ((n : ℕ) : K)] : from_zeta_aut hμ h (zeta n K L) = μ :=
+lemma from_zeta_aut_spec : from_zeta_aut hμ h (zeta n K L) = μ :=
 begin
   simp_rw [from_zeta_aut, aut_equiv_pow_symm_apply],
   generalize_proofs _ _ hζ h _ hμ _,
@@ -157,17 +153,17 @@ section gal
 variables (h : irreducible (cyclotomic n K)) {K}
 
 /-- `is_cyclotomic_extension.aut_equiv_pow` repackaged in terms of `gal`. Asserts that the
-Galois group of `cyclotomic n K` is equivalent to `(zmod n)ˣ` if `n` does not divide the
-characteristic of `K`, and `cyclotomic n K` is irreducible in the base field. -/
-noncomputable def gal_cyclotomic_equiv_units_zmod [ne_zero ((n : ℕ) : K)] :
+Galois group of `cyclotomic n K` is equivalent to `(zmod n)ˣ` if `cyclotomic n K` is irreducible in
+the base field. -/
+noncomputable def gal_cyclotomic_equiv_units_zmod :
   (cyclotomic n K).gal ≃* (zmod n)ˣ :=
 (alg_equiv.aut_congr (is_splitting_field.alg_equiv _ _)).symm.trans
 (is_cyclotomic_extension.aut_equiv_pow L h)
 
 /-- `is_cyclotomic_extension.aut_equiv_pow` repackaged in terms of `gal`. Asserts that the
-Galois group of `X ^ n - 1` is equivalent to `(zmod n)ˣ` if `n` does not divide the characteristic
-of `K`, and `cyclotomic n K` is irreducible in the base field. -/
-noncomputable def gal_X_pow_equiv_units_zmod [ne_zero ((n : ℕ) : K)] :
+Galois group of `X ^ n - 1` is equivalent to `(zmod n)ˣ` if `cyclotomic n K` is irreducible in the
+base field. -/
+noncomputable def gal_X_pow_equiv_units_zmod :
   (X ^ (n : ℕ) - 1).gal ≃* (zmod n)ˣ :=
 (alg_equiv.aut_congr (is_splitting_field.alg_equiv _ _)).symm.trans
 (is_cyclotomic_extension.aut_equiv_pow L h)
diff --git a/src/number_theory/cyclotomic/primitive_roots.lean b/src/number_theory/cyclotomic/primitive_roots.lean
index 2875e5286b771..3be3b8787f591 100644
--- a/src/number_theory/cyclotomic/primitive_roots.lean
+++ b/src/number_theory/cyclotomic/primitive_roots.lean
@@ -22,14 +22,13 @@ in the implementation details section.
 * `is_cyclotomic_extension.zeta n A B`: if `is_cyclotomic_extension {n} A B`, than `zeta n A B`
   is an element of `B` that plays the role of a primitive `n`-th root of unity.
 * `is_primitive_root.power_basis`: if `K` and `L` are fields such that
-  `is_cyclotomic_extension {n} K L` and `ne_zero (↑n : K)`, then `is_primitive_root.power_basis`
+  `is_cyclotomic_extension {n} K L`, then `is_primitive_root.power_basis`
   gives a K-power basis for L given a primitive root `ζ`.
 * `is_primitive_root.embeddings_equiv_primitive_roots`: the equivalence between `L →ₐ[K] A`
   and `primitive_roots n A` given by the choice of `ζ`.
 
 ## Main results
-* `is_cyclotomic_extension.zeta_primitive_root`: if `is_domain B` and `ne_zero (↑n : B)`, then
-  `zeta n A B` is a primitive `n`-th root of unity.
+* `is_cyclotomic_extension.zeta_primitive_root`: `zeta n A B` is a primitive `n`-th root of unity.
 * `is_cyclotomic_extension.finrank`: if `irreducible (cyclotomic n K)` (in particular for
   `K = ℚ`), then the `finrank` of a cyclotomic extension is `n.totient`.
 * `is_primitive_root.norm_eq_one`: if `irreducible (cyclotomic n K)` (in particular for `K = ℚ`),
@@ -48,9 +47,9 @@ in the implementation details section.
   and `primitive_roots n A` given by the choice of `ζ`.
 
 ## Implementation details
-`zeta n A B` is defined as any root of `cyclotomic n A` in `B`, that exists because of
-`is_cyclotomic_extension {n} A B`. It is not true in general that it is a primitive `n`-th root of
-unity, but this holds if `is_domain B` and `ne_zero (↑n : B)`.
+`zeta n A B` is defined as any primitive root of unity in `B`, that exists by definition. It is not
+true in general that it is a root of `cyclotomic n B`, but this holds if `is_domain B` and
+`ne_zero (↑n : B)`.
 
 `zeta n A B` is defined using `exists.some`, which means we cannot control it.
 For example, in normal mathematics, we can demand that `(zeta p ℤ ℤ[ζₚ] : ℚ(ζₚ))` is equal to
@@ -63,7 +62,6 @@ and only at the "final step", when we need to provide an "explicit" primitive ro
 
 open polynomial algebra finset finite_dimensional is_cyclotomic_extension nat pnat set
 
-
 universes u v w z
 
 variables {p n : ℕ+} (A : Type w) (B : Type z) (K : Type u) {L : Type v} (C : Type w)
@@ -75,25 +73,28 @@ namespace is_cyclotomic_extension
 
 variables (n)
 
-/-- If `B` is a `n`-th cyclotomic extension of `A`, then `zeta n A B` is any root of
-`cyclotomic n A` in L. -/
+/-- If `B` is a `n`-th cyclotomic extension of `A`, then `zeta n A B` is a primitive root of
+unity in `B`. -/
 noncomputable def zeta : B :=
-  (exists_root $ set.mem_singleton n : ∃ r : B, aeval r (cyclotomic n A) = 0).some
+(exists_prim_root A $ set.mem_singleton n : ∃ r : B, is_primitive_root r n).some
+
+/-- `zeta n A B` is a primitive `n`-th root of unity. -/
+@[simp] lemma zeta_spec : is_primitive_root (zeta n A B) n :=
+classical.some_spec (exists_prim_root A (set.mem_singleton n) : ∃ r : B, is_primitive_root r n)
 
-@[simp] lemma zeta_spec : aeval (zeta n A B) (cyclotomic n A) = 0 :=
-classical.some_spec (exists_root (set.mem_singleton n) : ∃ r : B, aeval r (cyclotomic n A) = 0)
+lemma aeval_zeta [is_domain B] [ne_zero ((n : ℕ) : B)] :
+  aeval (zeta n A B) (cyclotomic n A) = 0 :=
+begin
+  rw [aeval_def,  ← eval_map, ← is_root.def, map_cyclotomic, is_root_cyclotomic_iff],
+  exact zeta_spec n A B
+end
 
-lemma zeta_spec' : is_root (cyclotomic n B) (zeta n A B) :=
-by { convert zeta_spec n A B, rw [is_root.def, aeval_def, eval₂_eq_eval_map, map_cyclotomic] }
+lemma zeta_is_root [is_domain B] [ne_zero ((n : ℕ) : B)] :
+  is_root (cyclotomic n B) (zeta n A B) :=
+by { convert aeval_zeta n A B, rw [is_root.def, aeval_def, eval₂_eq_eval_map, map_cyclotomic] }
 
 lemma zeta_pow : (zeta n A B) ^ (n : ℕ) = 1 :=
-is_root_of_unity_of_root_cyclotomic (nat.mem_divisors_self _ n.pos.ne') (zeta_spec' _ _ _)
-
-/-- If `is_domain B` and `ne_zero (↑n : B)` then `zeta n A B` is a primitive `n`-th root of
-unity. -/
-lemma zeta_primitive_root [is_domain B] [ne_zero ((n : ℕ) : B)] :
-  is_primitive_root (zeta n A B) n :=
-by { rw ←is_root_cyclotomic_iff, exact zeta_spec' n A B }
+(zeta_spec n A B).pow_eq_one
 
 end is_cyclotomic_extension
 
@@ -111,7 +112,7 @@ variable {C}
 /-- The `power_basis` given by a primitive root `η`. -/
 @[simps] protected noncomputable def power_basis : power_basis K L :=
 power_basis.map (algebra.adjoin.power_basis $ integral {n} K L ζ) $
-  (subalgebra.equiv_of_eq _ _ (is_cyclotomic_extension.adjoin_primitive_root_eq_top n _ hζ)).trans
+  (subalgebra.equiv_of_eq _ _ (is_cyclotomic_extension.adjoin_primitive_root_eq_top hζ)).trans
   subalgebra.top_equiv
 
 lemma power_basis_gen_mem_adjoin_zeta_sub_one :
@@ -131,11 +132,11 @@ variables {K} (C)
 
 /-- The equivalence between `L →ₐ[K] C` and `primitive_roots n C` given by a primitive root `ζ`. -/
 @[simps] noncomputable def embeddings_equiv_primitive_roots (C : Type*) [comm_ring C] [is_domain C]
-  [algebra K C] [ne_zero ((n : ℕ) : K)]
-  (hirr : irreducible (cyclotomic n K)) : (L →ₐ[K] C) ≃ primitive_roots n C :=
+  [algebra K C] (hirr : irreducible (cyclotomic n K)) : (L →ₐ[K] C) ≃ primitive_roots n C :=
 ((hζ.power_basis K).lift_equiv).trans
 { to_fun    := λ x,
   begin
+    haveI := is_cyclotomic_extension.ne_zero' n K L,
     haveI hn := ne_zero.of_no_zero_smul_divisors K C n,
     refine ⟨x.1, _⟩,
     cases x,
@@ -145,6 +146,7 @@ variables {K} (C)
   end,
   inv_fun   := λ x,
   begin
+    haveI := is_cyclotomic_extension.ne_zero' n K L,
     haveI hn := ne_zero.of_no_zero_smul_divisors K C n,
     refine ⟨x.1, _⟩,
     cases x,
@@ -163,12 +165,12 @@ variables {K} (L)
 
 /-- If `irreducible (cyclotomic n K)` (in particular for `K = ℚ`), then the `finrank` of a
 cyclotomic extension is `n.totient`. -/
-lemma finrank (hirr : irreducible (cyclotomic n K)) [ne_zero ((n : ℕ) : K)] :
+lemma finrank (hirr : irreducible (cyclotomic n K)) :
   finrank K L = (n : ℕ).totient :=
 begin
-  haveI := ne_zero.of_no_zero_smul_divisors K L n,
-  rw [((zeta_primitive_root n K L).power_basis K).finrank, is_primitive_root.power_basis_dim,
-      ←(zeta_primitive_root n K L).minpoly_eq_cyclotomic_of_irreducible hirr, nat_degree_cyclotomic]
+  haveI := is_cyclotomic_extension.ne_zero' n K L,
+  rw [((zeta_spec n K L).power_basis K).finrank, is_primitive_root.power_basis_dim,
+      ←(zeta_spec n K L).minpoly_eq_cyclotomic_of_irreducible hirr, nat_degree_cyclotomic]
 end
 
 end is_cyclotomic_extension
@@ -180,7 +182,7 @@ section norm
 namespace is_primitive_root
 
 variables [field L] {ζ : L} (hζ : is_primitive_root ζ n)
-variables {K} [field K] [algebra K L] [ne_zero ((n : ℕ) : K)]
+variables {K} [field K] [algebra K L]
 
 /-- This mathematically trivial result is complementary to `norm_eq_one` below. -/
 lemma norm_eq_neg_one_pow (hζ : is_primitive_root ζ 2) : norm K ζ = (-1) ^ finrank K L :=
@@ -194,6 +196,7 @@ include hζ
 lemma norm_eq_one [is_cyclotomic_extension {n} K L] (hn : n ≠ 2)
   (hirr : irreducible (cyclotomic n K)) : norm K ζ = 1 :=
 begin
+  haveI := is_cyclotomic_extension.ne_zero' n K L,
   by_cases h1 : n = 1,
   { rw [h1, one_coe, one_right_iff] at hζ,
     rw [hζ, show 1 = algebra_map K L 1, by simp, algebra.norm_algebra_map, one_pow] },
@@ -210,7 +213,6 @@ end
 lemma norm_eq_one_of_linearly_ordered {K : Type*} [linear_ordered_field K] [algebra K L]
   (hodd : odd (n : ℕ)) : norm K ζ = 1 :=
 begin
-  haveI := ne_zero.of_no_zero_smul_divisors K L n,
   have hz := congr_arg (norm K) ((is_primitive_root.iff_def _ n).1 hζ).1,
   rw [←(algebra_map K L).map_one , algebra.norm_algebra_map, one_pow, map_pow, ←one_pow ↑n] at hz,
   exact strict_mono.injective hodd.strict_mono_pow hz
@@ -227,21 +229,13 @@ begin
   { exact hζ.norm_eq_one hn hirr }
 end
 
-lemma minpoly_sub_one_eq_cyclotomic_comp [is_cyclotomic_extension {n} K L]
-  (h : irreducible (polynomial.cyclotomic n K)) :
-  minpoly K (ζ - 1) = (cyclotomic n K).comp (X + 1) :=
-begin
-  rw [show ζ - 1 = ζ + (algebra_map K L (-1)), by simp [sub_eq_add_neg], minpoly.add_algebra_map
-    (is_cyclotomic_extension.integral {n} K L ζ), hζ.minpoly_eq_cyclotomic_of_irreducible h],
-  simp
-end
-
 /-- If `irreducible (cyclotomic n K)` (in particular for `K = ℚ`), then the norm of
 `ζ - 1` is `eval 1 (cyclotomic n ℤ)`. -/
 lemma sub_one_norm_eq_eval_cyclotomic [is_cyclotomic_extension {n} K L]
   (h : 2 < (n : ℕ)) (hirr : irreducible (cyclotomic n K)) :
   norm K (ζ - 1) = ↑(eval 1 (cyclotomic n ℤ)) :=
 begin
+  haveI := is_cyclotomic_extension.ne_zero' n K L,
   let E := algebraic_closure L,
   obtain ⟨z, hz⟩ := is_alg_closed.exists_root _ (degree_cyclotomic_pos n E n.pos).ne.symm,
   apply (algebra_map K E).injective,
@@ -282,27 +276,30 @@ end
 
 omit hζ
 
+variable {A}
+
+lemma minpoly_sub_one_eq_cyclotomic_comp [algebra K A] [is_domain A] {ζ : A}
+  [is_cyclotomic_extension {n} K A] (hζ : is_primitive_root ζ n)
+  (h : irreducible (polynomial.cyclotomic n K)) :
+  minpoly K (ζ - 1) = (cyclotomic n K).comp (X + 1) :=
+begin
+  haveI := is_cyclotomic_extension.ne_zero' n K A,
+  rw [show ζ - 1 = ζ + (algebra_map K A (-1)), by simp [sub_eq_add_neg], minpoly.add_algebra_map
+    (is_cyclotomic_extension.integral {n} K A ζ), hζ.minpoly_eq_cyclotomic_of_irreducible h],
+  simp
+end
+
 local attribute [instance] is_cyclotomic_extension.finite_dimensional
 local attribute [instance] is_cyclotomic_extension.is_galois
 
 /-- If `irreducible (cyclotomic (p ^ (k + 1)) K)` (in particular for `K = ℚ`) and `p` is a prime,
 then the norm of `ζ ^ (p ^ s) - 1` is `p ^ (p ^ s)` if `p ^ (k - s + 1) ≠ 2`. See the next lemmas
 for similar results. -/
-lemma pow_sub_one_norm_prime_pow_ne_two [ne_zero ((p : ℕ) : K)] {k s : ℕ}
-  (hζ : is_primitive_root ζ ↑(p ^ (k + 1))) [hpri : fact (p : ℕ).prime]
-  [is_cyclotomic_extension {p ^ (k + 1)} K L]
+lemma pow_sub_one_norm_prime_pow_ne_two {k s : ℕ} (hζ : is_primitive_root ζ ↑(p ^ (k + 1)))
+  [hpri : fact (p : ℕ).prime] [is_cyclotomic_extension {p ^ (k + 1)} K L]
   (hirr : irreducible (cyclotomic (↑(p ^ (k + 1)) : ℕ) K)) (hs : s ≤ k)
   (htwo : p ^ (k - s + 1) ≠ 2) : norm K (ζ ^ ((p : ℕ) ^ s) - 1) = p ^ ((p : ℕ) ^ s) :=
 begin
-  haveI : ne_zero ((↑(p ^ (k + 1)) : ℕ) : K),
-  { refine ⟨λ hzero, _⟩,
-    rw [pnat.pow_coe] at hzero,
-    simpa [ne_zero.ne ((p : ℕ) : K)] using hzero },
-  haveI : ne_zero ((↑(p ^ (k - s + 1)) : ℕ) : K),
-  { refine ⟨λ hzero, _⟩,
-    rw [pnat.pow_coe] at hzero,
-    simpa [ne_zero.ne ((p : ℕ) : K)] using hzero },
-
   have hirr₁ : irreducible (cyclotomic (p ^ (k - s + 1)) K) :=
   cyclotomic_irreducible_pow_of_irreducible_pow hpri.1 (by linarith) hirr,
   rw ←pnat.pow_coe at hirr₁,
@@ -357,9 +354,8 @@ end
 
 /-- If `irreducible (cyclotomic (p ^ (k + 1)) K)` (in particular for `K = ℚ`) and `p` is a prime,
 then the norm of `ζ ^ (p ^ s) - 1` is `p ^ (p ^ s)` if `p ≠ 2`. -/
-lemma pow_sub_one_norm_prime_ne_two [ne_zero ((p : ℕ) : K)] {k : ℕ}
-  (hζ : is_primitive_root ζ ↑(p ^ (k + 1))) [hpri : fact (p : ℕ).prime]
-  [is_cyclotomic_extension {p ^ (k + 1)} K L]
+lemma pow_sub_one_norm_prime_ne_two {k : ℕ} (hζ : is_primitive_root ζ ↑(p ^ (k + 1)))
+  [hpri : fact (p : ℕ).prime] [is_cyclotomic_extension {p ^ (k + 1)} K L]
   (hirr : irreducible (cyclotomic (↑(p ^ (k + 1)) : ℕ) K)) {s : ℕ} (hs : s ≤ k)
   (hodd : p ≠ 2) : norm K (ζ ^ ((p : ℕ) ^ s) - 1) = p ^ ((p : ℕ) ^ s) :=
 begin
@@ -373,39 +369,31 @@ end
 
 /-- If `irreducible (cyclotomic (p ^ (k + 1)) K)` (in particular for `K = ℚ`) and `p` is an odd
 prime, then the norm of `ζ - 1` is `p`. -/
-lemma sub_one_norm_prime_ne_two [ne_zero ((p : ℕ) : K)] {k : ℕ}
-  (hζ : is_primitive_root ζ ↑(p ^ (k + 1))) [hpri : fact (p : ℕ).prime]
-  [is_cyclotomic_extension {p ^ (k + 1)} K L]
+lemma sub_one_norm_prime_ne_two {k : ℕ} (hζ : is_primitive_root ζ ↑(p ^ (k + 1)))
+  [hpri : fact (p : ℕ).prime] [is_cyclotomic_extension {p ^ (k + 1)} K L]
   (hirr : irreducible (cyclotomic (↑(p ^ (k + 1)) : ℕ) K)) (h : p ≠ 2) :
   norm K (ζ - 1) = p :=
 by simpa using hζ.pow_sub_one_norm_prime_ne_two hirr k.zero_le h
 
 /-- If `irreducible (cyclotomic p K)` (in particular for `K = ℚ`) and `p` is an odd prime,
 then the norm of `ζ - 1` is `p`. -/
-lemma sub_one_norm_prime [ne_zero ((p : ℕ) : K)] [hpri : fact (p : ℕ).prime]
-  [hcyc : is_cyclotomic_extension {p} K L] (hζ: is_primitive_root ζ p)
-  (hirr : irreducible (cyclotomic p K)) (h : p ≠ 2) :
+lemma sub_one_norm_prime [hpri : fact (p : ℕ).prime] [hcyc : is_cyclotomic_extension {p} K L]
+  (hζ: is_primitive_root ζ p) (hirr : irreducible (cyclotomic p K)) (h : p ≠ 2) :
   norm K (ζ - 1) = p :=
 begin
   replace hirr : irreducible (cyclotomic (↑(p ^ (0 + 1)) : ℕ) K) := by simp [hirr],
   replace hζ : is_primitive_root ζ (↑(p ^ (0 + 1)) : ℕ) := by simp [hζ],
-  haveI : ne_zero ((↑(p ^ (0 + 1)) : ℕ) : K) := ⟨by simp [ne_zero.ne ((p : ℕ) : K)]⟩,
   haveI : is_cyclotomic_extension {p ^ (0 + 1)} K L := by simp [hcyc],
   simpa using sub_one_norm_prime_ne_two hζ hirr h
 end
 
 /-- If `irreducible (cyclotomic (2 ^ (k + 1)) K)` (in particular for `K = ℚ`), then the norm of
 `ζ ^ (2 ^ k) - 1` is `(-2) ^ (2 ^ k)`. -/
-lemma pow_sub_one_norm_two [ne_zero (2 : K)] {k : ℕ} (hζ : is_primitive_root ζ (2 ^ (k + 1)))
+lemma pow_sub_one_norm_two {k : ℕ} (hζ : is_primitive_root ζ (2 ^ (k + 1)))
   [is_cyclotomic_extension {2 ^ (k + 1)} K L]
   (hirr : irreducible (cyclotomic (2 ^ (k + 1)) K)) :
   norm K (ζ ^ (2 ^ k) - 1) = (-2) ^ (2 ^ k) :=
 begin
-  haveI : ne_zero (((2 ^ (k + 1) : ℕ+) : ℕ) : K),
-  { refine ⟨λ hzero, _⟩,
-    rw [pow_coe, pnat.coe_bit0, one_coe, cast_pow, cast_bit0, cast_one] at hzero,
-    exact (ne_zero.ne (2 : K)) (pow_eq_zero hzero) },
-
   have := hζ.pow_of_dvd (λ h, two_ne_zero (pow_eq_zero h)) (pow_dvd_pow 2 (le_succ k)),
   rw [nat.pow_div (le_succ k) zero_lt_two, nat.succ_sub (le_refl k), nat.sub_self, pow_one] at this,
   have H : (-1 : L) - (1 : L) = algebra_map K L (-2),
@@ -420,16 +408,10 @@ end
 
 /-- If `irreducible (cyclotomic (2 ^ k) K)` (in particular for `K = ℚ`) and `k` is at least `2`,
 then the norm of `ζ - 1` is `2`. -/
-lemma sub_one_norm_two [ne_zero (2 : K)] {k : ℕ} (hζ : is_primitive_root ζ (2 ^ k))
-  (hk : 2 ≤ k) [H : is_cyclotomic_extension {2 ^ k} K L]
-  (hirr : irreducible (cyclotomic (2 ^ k) K)) : norm K (ζ - 1) = 2 :=
+lemma sub_one_norm_two {k : ℕ} (hζ : is_primitive_root ζ (2 ^ k)) (hk : 2 ≤ k)
+  [H : is_cyclotomic_extension {2 ^ k} K L] (hirr : irreducible (cyclotomic (2 ^ k) K)) :
+  norm K (ζ - 1) = 2 :=
 begin
-  haveI : ne_zero (((2 ^ k : ℕ+) : ℕ) : K),
-  { refine ⟨λ hzero, _⟩,
-    rw [pow_coe, pnat.coe_bit0, one_coe, cast_pow, cast_bit0, cast_one,
-      pow_eq_zero_iff (lt_of_lt_of_le zero_lt_two hk)] at hzero,
-    exact (ne_zero.ne (2 : K)) hzero,
-    apply_instance },
   have : 2 < (2 ^ k : ℕ+),
   { simp only [← coe_lt_coe, pnat.coe_bit0, one_coe, pow_coe],
     nth_rewrite 0 [← pow_one 2],
@@ -442,9 +424,8 @@ end
 
 /-- If `irreducible (cyclotomic (p ^ (k + 1)) K)` (in particular for `K = ℚ`) and `p` is a prime,
 then the norm of `ζ ^ (p ^ s) - 1` is `p ^ (p ^ s)` if `1 ≤ k`. -/
-lemma pow_sub_one_norm_prime_pow_of_one_le [hne : ne_zero ((p : ℕ) : K)] {k s : ℕ}
-  (hζ : is_primitive_root ζ ↑(p ^ (k + 1))) [hpri : fact (p : ℕ).prime]
-  [hcycl : is_cyclotomic_extension {p ^ (k + 1)} K L]
+lemma pow_sub_one_norm_prime_pow_of_one_le {k s : ℕ} (hζ : is_primitive_root ζ ↑(p ^ (k + 1)))
+  [hpri : fact (p : ℕ).prime] [hcycl : is_cyclotomic_extension {p ^ (k + 1)} K L]
   (hirr : irreducible (cyclotomic (↑(p ^ (k + 1)) : ℕ) K)) (hs : s ≤ k)
   (hk : 1 ≤ k) : norm K (ζ ^ ((p : ℕ) ^ s) - 1) = p ^ ((p : ℕ) ^ s) :=
 begin
@@ -460,10 +441,6 @@ begin
       replace htwo := nat.pow_right_injective rfl.le htwo,
       rw [add_left_eq_self, nat.sub_eq_zero_iff_le] at htwo,
       refine le_antisymm hs htwo },
-    haveI : ne_zero (2 : K),
-    { refine ⟨λ h, _⟩,
-      rw [hp, pnat.coe_bit0, one_coe, cast_bit0, cast_one, h] at hne,
-      simpa using hne.out },
     simp only [hs, hp, pnat.coe_bit0, one_coe, coe_coe, cast_bit0, cast_one,
       pow_coe] at ⊢ hζ hirr hcycl,
     haveI := hcycl,
@@ -480,16 +457,12 @@ namespace is_cyclotomic_extension
 
 open is_primitive_root
 
-variables {K} (L) [field K] [field L] [algebra K L] [ne_zero ((n : ℕ) : K)]
-
+variables {K} (L) [field K] [field L] [algebra K L]
 /-- If `irreducible (cyclotomic n K)` (in particular for `K = ℚ`), the norm of `zeta n K L` is `1`
 if `n` is odd. -/
 lemma norm_zeta_eq_one [is_cyclotomic_extension {n} K L] (hn : n ≠ 2)
   (hirr : irreducible (cyclotomic n K)) : norm K (zeta n K L) = 1 :=
-begin
-  haveI := ne_zero.of_no_zero_smul_divisors K L n,
-  exact (zeta_primitive_root n K L).norm_eq_one hn hirr,
-end
+(zeta_spec n K L).norm_eq_one hn hirr
 
 /-- If `is_prime_pow (n : ℕ)`, `n ≠ 2` and `irreducible (cyclotomic n K)` (in particular for
 `K = ℚ`), then the norm of `zeta n K L - 1` is `(n : ℕ).min_fac`. -/
@@ -497,70 +470,39 @@ lemma is_prime_pow_norm_zeta_sub_one (hn : is_prime_pow (n : ℕ))
   [is_cyclotomic_extension {n} K L]
   (hirr : irreducible (cyclotomic (n : ℕ) K)) (h : n ≠ 2) :
   norm K (zeta n K L - 1) = (n : ℕ).min_fac :=
-begin
-  haveI := ne_zero.of_no_zero_smul_divisors K L n,
-  exact (zeta_primitive_root n K L).sub_one_norm_is_prime_pow hn hirr h,
-end
+(zeta_spec n K L).sub_one_norm_is_prime_pow hn hirr h
 
 /-- If `irreducible (cyclotomic (p ^ (k + 1)) K)` (in particular for `K = ℚ`) and `p` is a prime,
 then the norm of `(zeta (p ^ (k + 1)) K L) ^ (p ^ s) - 1` is `p ^ (p ^ s)`
 if `p ^ (k - s + 1) ≠ 2`. -/
-lemma prime_ne_two_pow_norm_zeta_pow_sub_one [ne_zero ((p : ℕ) : K)] {k : ℕ}
-  [hpri : fact (p : ℕ).prime]
+lemma prime_ne_two_pow_norm_zeta_pow_sub_one {k : ℕ} [hpri : fact (p : ℕ).prime]
   [is_cyclotomic_extension {p ^ (k + 1)} K L]
   (hirr : irreducible (cyclotomic (↑(p ^ (k + 1)) : ℕ) K))  {s : ℕ} (hs : s ≤ k)
   (htwo : p ^ (k - s + 1) ≠ 2) :
   norm K ((zeta (p ^ (k + 1)) K L) ^ ((p : ℕ) ^ s) - 1) = p ^ ((p : ℕ) ^ s) :=
-begin
-  haveI := ne_zero.of_no_zero_smul_divisors K L p,
-  haveI : ne_zero ((↑(p ^ (k + 1)) : ℕ) : L),
-  { refine ⟨λ hzero, _⟩,
-    rw [pow_coe] at hzero,
-    simpa [ne_zero.ne ((p : ℕ) : L)] using hzero },
-  exact (zeta_primitive_root _ K L).pow_sub_one_norm_prime_pow_ne_two hirr hs htwo
-end
+(zeta_spec _ K L).pow_sub_one_norm_prime_pow_ne_two hirr hs htwo
 
 /-- If `irreducible (cyclotomic (p ^ (k + 1)) K)` (in particular for `K = ℚ`) and `p` is an odd
 prime, then the norm of `zeta (p ^ (k + 1)) K L - 1` is `p`. -/
-lemma prime_ne_two_pow_norm_zeta_sub_one [ne_zero ((p : ℕ) : K)] {k : ℕ}
-  [hpri : fact (p : ℕ).prime] [is_cyclotomic_extension {p ^ (k + 1)} K L]
+lemma prime_ne_two_pow_norm_zeta_sub_one {k : ℕ} [hpri : fact (p : ℕ).prime]
+  [is_cyclotomic_extension {p ^ (k + 1)} K L]
   (hirr : irreducible (cyclotomic (↑(p ^ (k + 1)) : ℕ) K)) (h : p ≠ 2) :
   norm K (zeta (p ^ (k + 1)) K L - 1) = p :=
-begin
-  haveI := ne_zero.of_no_zero_smul_divisors K L p,
-  haveI : ne_zero ((↑(p ^ (k + 1)) : ℕ) : L),
-  { refine ⟨λ hzero, _⟩,
-    rw [pow_coe] at hzero,
-    simpa [ne_zero.ne ((p : ℕ) : L)] using hzero },
-  exact (zeta_primitive_root _ K L).sub_one_norm_prime_ne_two hirr h,
-end
+(zeta_spec _ K L).sub_one_norm_prime_ne_two hirr h
 
 /-- If `irreducible (cyclotomic p K)` (in particular for `K = ℚ`) and `p` is an odd prime,
 then the norm of `zeta p K L - 1` is `p`. -/
-lemma prime_ne_two_norm_zeta_sub_one [ne_zero ((p : ℕ) : K)] [hpri : fact (p : ℕ).prime]
+lemma prime_ne_two_norm_zeta_sub_one [hpri : fact (p : ℕ).prime]
   [hcyc : is_cyclotomic_extension {p} K L] (hirr : irreducible (cyclotomic p K)) (h : p ≠ 2) :
   norm K (zeta p K L - 1) = p :=
-begin
-  haveI := ne_zero.of_no_zero_smul_divisors K L p,
-  exact (zeta_primitive_root _ K L).sub_one_norm_prime hirr h,
-end
+(zeta_spec _ K L).sub_one_norm_prime hirr h
 
 /-- If `irreducible (cyclotomic (2 ^ k) K)` (in particular for `K = ℚ`) and `k` is at least `2`,
 then the norm of `zeta (2 ^ k) K L - 1` is `2`. -/
-lemma two_pow_norm_zeta_sub_one [ne_zero (2 : K)] {k : ℕ} (hk : 2 ≤ k)
+lemma two_pow_norm_zeta_sub_one {k : ℕ} (hk : 2 ≤ k)
   [is_cyclotomic_extension {2 ^ k} K L] (hirr : irreducible (cyclotomic (2 ^ k) K)) :
   norm K (zeta (2 ^ k) K L - 1) = 2 :=
-begin
-  haveI : ne_zero (((2 ^ k : ℕ+) : ℕ) : L),
-  { refine ⟨λ hzero, _⟩,
-    rw [pow_coe, pnat.coe_bit0, one_coe, cast_pow, cast_bit0, cast_one, pow_eq_zero_iff
-      (lt_of_lt_of_le zero_lt_two hk), show (2 : L) = algebra_map K L 2, by simp,
-      show (0 : L) = algebra_map K L 0, by simp] at hzero,
-    exact (ne_zero.ne (2 : K)) ((algebra_map K L).injective hzero),
-    apply_instance },
-  refine sub_one_norm_two _ hk hirr,
-  simpa using zeta_primitive_root (2 ^ k) K L,
-end
+sub_one_norm_two (zeta_spec (2 ^ k) K L) hk hirr
 
 end is_cyclotomic_extension
 
diff --git a/src/number_theory/cyclotomic/rat.lean b/src/number_theory/cyclotomic/rat.lean
index d02a490ee2967..0c49b9fa460c7 100644
--- a/src/number_theory/cyclotomic/rat.lean
+++ b/src/number_theory/cyclotomic/rat.lean
@@ -110,6 +110,7 @@ begin
       rw [is_primitive_root.sub_one_power_basis_gen] at h₁,
       rw [h₁, ← map_cyclotomic_int, show int.cast_ring_hom ℚ = algebra_map ℤ ℚ, by refl,
         show ((X + 1)) = map (algebra_map ℤ ℚ) (X + 1), by simp, ← map_comp] at h₂,
+      haveI : char_zero ℚ := ordered_semiring.to_char_zero,
       rw [is_primitive_root.sub_one_power_basis_gen, map_injective (algebra_map ℤ ℚ)
         ((algebra_map ℤ ℚ).injective_int) h₂],
       exact cyclotomic_prime_pow_comp_X_add_one_is_eisenstein_at _ _ },
@@ -135,11 +136,12 @@ local attribute [instance] algebra_rat_subsingleton
 lemma cyclotomic_ring_is_integral_closure_of_prime_pow :
   is_integral_closure (cyclotomic_ring (p ^ k) ℤ ℚ) ℤ (cyclotomic_field (p ^ k) ℚ) :=
 begin
+  haveI : char_zero ℚ := ordered_semiring.to_char_zero,
   haveI : is_cyclotomic_extension {p ^ k} ℚ (cyclotomic_field (p ^ k) ℚ),
   { convert cyclotomic_field.is_cyclotomic_extension (p ^ k) _,
     { exact subsingleton.elim _ _ },
     { exact ne_zero.char_zero } },
-  have hζ := zeta_primitive_root (p ^ k) ℚ (cyclotomic_field (p ^ k) ℚ),
+  have hζ := zeta_spec (p ^ k) ℚ (cyclotomic_field (p ^ k) ℚ),
   refine ⟨is_fraction_ring.injective _ _, λ x, ⟨λ h, ⟨⟨x, _⟩, rfl⟩, _⟩⟩,
   { have := (is_integral_closure_adjoing_singleton_of_prime_pow hζ).is_integral_iff,
     obtain ⟨y, rfl⟩ := this.1 h,
diff --git a/src/ring_theory/polynomial/cyclotomic/eval.lean b/src/ring_theory/polynomial/cyclotomic/eval.lean
index 5ebd163d8e51d..663a986e26461 100644
--- a/src/ring_theory/polynomial/cyclotomic/eval.lean
+++ b/src/ring_theory/polynomial/cyclotomic/eval.lean
@@ -136,7 +136,7 @@ lemma cyclotomic_nonneg (n : ℕ) {R} [linear_ordered_comm_ring R] {x : R} (hx :
   0 ≤ eval x (cyclotomic n R) :=
 (cyclotomic_pos_and_nonneg n x).2 hx
 
-lemma eval_one_cyclotomic_not_prime_pow {R : Type*} [comm_ring R] {n : ℕ}
+lemma eval_one_cyclotomic_not_prime_pow {R : Type*} [ring R] {n : ℕ}
   (h : ∀ {p : ℕ}, p.prime → ∀ k : ℕ, p ^ k ≠ n) : eval 1 (cyclotomic n R) = 1 :=
 begin
   rcases n.eq_zero_or_pos with rfl | hn',
diff --git a/src/ring_theory/roots_of_unity.lean b/src/ring_theory/roots_of_unity.lean
index ce30e6fedd5e6..42dc000433993 100644
--- a/src/ring_theory/roots_of_unity.lean
+++ b/src/ring_theory/roots_of_unity.lean
@@ -84,6 +84,10 @@ def roots_of_unity (k : ℕ+) (M : Type*) [comm_monoid M] : subgroup Mˣ :=
 @[simp] lemma mem_roots_of_unity (k : ℕ+) (ζ : Mˣ) :
   ζ ∈ roots_of_unity k M ↔ ζ ^ (k : ℕ) = 1 := iff.rfl
 
+lemma mem_roots_of_unity' (k : ℕ+) (ζ : Mˣ) :
+  ζ ∈ roots_of_unity k M ↔ (ζ : M) ^ (k : ℕ) = 1 :=
+by { rw [mem_roots_of_unity], norm_cast }
+
 lemma roots_of_unity.coe_injective {n : ℕ+} : function.injective (coe : (roots_of_unity n M) → M) :=
 units.ext.comp (λ x y, subtype.ext)
 
@@ -232,6 +236,17 @@ end
 
 end is_domain
 
+section reduced
+
+variables (R) [comm_ring R] [is_reduced R]
+
+@[simp] lemma mem_roots_of_unity_prime_pow_mul_iff (p k : ℕ) (m : ℕ+) [hp : fact p.prime]
+  [char_p R p] {ζ : Rˣ} :
+  ζ ∈ roots_of_unity (⟨p, hp.1.pos⟩ ^ k * m) R ↔ ζ ∈ roots_of_unity m R :=
+by simp [mem_roots_of_unity']
+
+end reduced
+
 end roots_of_unity
 
 /-- An element `ζ` is a primitive `k`-th root of unity if `ζ ^ k = 1`,
@@ -590,6 +605,29 @@ begin
     exact hx }
 end
 
+lemma ne_zero' {n : ℕ+} (hζ : is_primitive_root ζ n) : ne_zero ((n : ℕ) : R) :=
+begin
+  let p := ring_char R,
+  have hfin := (multiplicity.finite_nat_iff.2 ⟨char_p.char_ne_one R p, n.pos⟩),
+  obtain ⟨m, hm⟩ := multiplicity.exists_eq_pow_mul_and_not_dvd hfin,
+  by_cases hp : p ∣ n,
+  { obtain ⟨k, hk⟩ := nat.exists_eq_succ_of_ne_zero (multiplicity.pos_of_dvd hfin hp).ne',
+    haveI hpri : fact p.prime :=
+      @char_p.char_is_prime_of_pos R _ _ _ p ⟨nat.pos_of_dvd_of_pos hp n.pos⟩ _,
+    have := hζ.pow_eq_one,
+    rw [hm.1, hk, pow_succ, mul_assoc, pow_mul', ← frobenius_def, ← frobenius_one p] at this,
+    exfalso,
+    have hpos : 0 < p ^ k * m,
+    { refine (mul_pos (pow_pos hpri.1.pos _) (nat.pos_of_ne_zero (λ h, _))),
+      have H := hm.1,
+      rw [h] at H,
+      simpa using H },
+    refine hζ.pow_ne_one_of_pos_of_lt hpos _ (frobenius_inj R p this),
+    { rw [hm.1, hk, pow_succ, mul_assoc, mul_comm p],
+      exact lt_mul_of_one_lt_right hpos hpri.1.one_lt } },
+  { exact ne_zero.of_not_dvd R hp }
+end
+
 end is_domain
 
 section is_domain