diff --git a/src/number_theory/cyclotomic/primitive_roots.lean b/src/number_theory/cyclotomic/primitive_roots.lean
index 840fc194d1d6d..93922bd038b1d 100644
--- a/src/number_theory/cyclotomic/primitive_roots.lean
+++ b/src/number_theory/cyclotomic/primitive_roots.lean
@@ -4,8 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Alex Best, Riccardo Brasca, Eric Rodriguez
 -/
 
+import algebra.is_prime_pow
 import number_theory.cyclotomic.basic
 import ring_theory.adjoin.power_basis
+import ring_theory.polynomial.cyclotomic.eval
 import ring_theory.norm
 
 /-!
@@ -31,8 +33,15 @@ in the implementation details section.
   `K = ℚ`), then the `finrank` of a cyclotomic extension is `n.totient`.
 * `is_primitive_root.norm_eq_one`: If `K` is linearly ordered (in particular for `K = ℚ`), the norm
   of a primitive root is `1` if `n` is odd.
-* `is_primitive_root.sub_one_norm_eq_eval_cyclotomic`: If `irreducible (cyclotomic n K)`, then
-  the norm of `ζ - 1` is `eval 1 (cyclotomic n ℤ)`.
+* `is_primitive_root.sub_one_norm_eq_eval_cyclotomic`: if `irreducible (cyclotomic n K)`
+  (in particular for `K = ℚ`), then the norm of `ζ - 1` is `eval 1 (cyclotomic n ℤ)`, for a
+  primitive root ζ. We also prove the analogous of this result for `zeta`.
+* `is_primitive_root.prime_ne_two_pow.sub_one_norm` : if `irreducible (cyclotomic (p ^ (k + 1)) K)`
+  (in particular for `K = ℚ`) and `p` is an odd prime, then the norm of `ζ - 1` is `p`. We also
+  prove the analogous of this result for `zeta`.
+  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 `ζ`.
 
 ## Implementation details
 `zeta n A B` is defined as any root of `cyclotomic n A` in `B`, that exists because of
@@ -48,7 +57,7 @@ and only at the "final step", when we need to provide an "explicit" primitive ro
 
 -/
 
-open polynomial algebra finset finite_dimensional is_cyclotomic_extension
+open polynomial algebra finset finite_dimensional is_cyclotomic_extension nat pnat
 
 
 universes u v w z
@@ -147,10 +156,10 @@ end is_cyclotomic_extension
 
 end no_order
 
-namespace is_primitive_root
-
 section norm
 
+namespace is_primitive_root
+
 variables [field L] {ζ : L} (hζ : is_primitive_root ζ n)
 
 include hζ
@@ -165,12 +174,12 @@ begin
   exact strict_mono.injective hodd.strict_mono_pow hz
 end
 
-variables {K}
+variables {K} [field K] [algebra K L] [ne_zero ((n : ℕ) : K)]
 
 /-- 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 [field K] [algebra K L] [is_cyclotomic_extension {n} K L]
-  [ne_zero ((n : ℕ) : K)] (h : 2 < (n : ℕ)) (hirr : irreducible (cyclotomic n K)) :
+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
   let E := algebraic_closure L,
@@ -182,7 +191,7 @@ begin
   conv_lhs { congr, skip, funext,
     rw [← neg_sub, alg_hom.map_neg, alg_hom.map_sub, alg_hom.map_one, neg_eq_neg_one_mul] },
   rw [prod_mul_distrib, prod_const, card_univ, alg_hom.card, is_cyclotomic_extension.finrank L hirr,
-      nat.neg_one_pow_of_even (nat.totient_even h), one_mul],
+      neg_one_pow_of_even (totient_even h), one_mul],
   have : univ.prod (λ (σ : L →ₐ[K] E), 1 - σ ζ) = eval 1 (cyclotomic' n E),
   { rw [cyclotomic', eval_prod, ← @finset.prod_attach E E, ← univ_eq_attach],
     refine fintype.prod_equiv (hζ.embeddings_equiv_primitive_roots E hirr) _ _ (λ σ, _),
@@ -193,6 +202,154 @@ begin
       ring_hom.eq_int_cast, int.cast_id]
 end
 
-end norm
+/-- If `is_prime_pow (n : ℕ)`, `n ≠ 2` and `irreducible (cyclotomic n K)` (in particular for
+`K = ℚ`), then the norm of `ζ - 1` is `(n : ℕ).min_fac`. -/
+lemma sub_one_norm.is_prime_pow (hn : is_prime_pow (n : ℕ)) [is_cyclotomic_extension {n} K L]
+  (hirr : irreducible (cyclotomic (n : ℕ) K)) (h : n ≠ 2) :
+  norm K (ζ - 1) = (n : ℕ).min_fac :=
+begin
+  have := (coe_lt_coe 2 _).1 (lt_of_le_of_ne (succ_le_of_lt (is_prime_pow.one_lt hn))
+    (function.injective.ne pnat.coe_injective h).symm),
+  letI hprime : fact ((n : ℕ).min_fac.prime) := ⟨min_fac_prime (is_prime_pow.ne_one hn)⟩,
+  rw [sub_one_norm_eq_eval_cyclotomic hζ this hirr],
+  nth_rewrite 0 [← is_prime_pow.min_fac_pow_factorization_eq hn],
+  obtain ⟨k, hk⟩ : ∃ k, ((n : ℕ).factorization) (n : ℕ).min_fac = k + 1 :=
+    exists_eq_succ_of_ne_zero (((n : ℕ).factorization.mem_support_to_fun (n : ℕ).min_fac).1 $
+      factor_iff_mem_factorization.2 $ (mem_factors (is_prime_pow.ne_zero hn)).2
+        ⟨hprime.out, min_fac_dvd _⟩),
+  simp [hk, sub_one_norm_eq_eval_cyclotomic hζ this hirr],
+end
+
+omit hζ
+
+/-- 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 prime_ne_two_pow.sub_one_norm {p : ℕ+} [ne_zero ((p : ℕ) : K)] (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 :=
+begin
+  haveI : ne_zero ((↑(p ^ (k + 1)) : ℕ) : K),
+  { refine ⟨λ hzero, _⟩,
+    rw [pow_coe] at hzero,
+    simpa [ne_zero.ne ((p : ℕ) : K)] using hzero },
+  have : 2 < p ^ (k + 1),
+  { rw [← coe_lt_coe, pow_coe, pnat.coe_bit0, one_coe],
+    calc 2 < (p : ℕ) : lt_of_le_of_ne hpri.1.two_le (by contrapose! h; exact coe_injective h.symm)
+      ...  = (p : ℕ) ^ 1 : (pow_one _).symm
+      ...  ≤ (p : ℕ) ^ (k + 1) : pow_le_pow (nat.prime.pos hpri.out) le_add_self },
+  simp [sub_one_norm_eq_eval_cyclotomic hζ this hirr]
+end
+
+/-- 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 {p : ℕ+} [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) :
+  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 prime_ne_two_pow.sub_one_norm 0 hζ hirr h
+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.pow_two [ne_zero (2 : K)] {k : ℕ} (hk : 2 ≤ k)
+  [is_cyclotomic_extension {2 ^ k} K L] (hζ : is_primitive_root ζ (2 ^ k))
+  (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],
+    exact pow_lt_pow one_lt_two (lt_of_lt_of_le one_lt_two hk) },
+  replace hirr : irreducible (cyclotomic (2 ^ k : ℕ+) K) := by simp [hirr],
+  replace hζ : is_primitive_root ζ (2 ^ k : ℕ+) := by simp [hζ],
+  obtain ⟨k₁, hk₁⟩ := exists_eq_succ_of_ne_zero ((lt_of_lt_of_le zero_lt_two hk).ne.symm),
+  simpa [hk₁] using sub_one_norm_eq_eval_cyclotomic hζ this hirr,
+end
 
 end is_primitive_root
+
+namespace is_cyclotomic_extension
+
+open is_primitive_root
+
+/-- If `K` is linearly ordered (in particular for `K = ℚ`), the norm of `zeta n K L` is `1`
+if `n` is odd. -/
+lemma norm_zeta_eq_one (K : Type u) [linear_ordered_field K] (L : Type v) [field L] [algebra K L]
+  [is_cyclotomic_extension {n} K L] (hodd : odd (n : ℕ)) : norm K (zeta n K L) = 1 :=
+begin
+  haveI := ne_zero.of_no_zero_smul_divisors K L n,
+  exact norm_eq_one K (zeta_primitive_root n K L) hodd,
+end
+
+variables {K} (L) [field K] [field L] [algebra K L] [ne_zero ((n : ℕ) : K)]
+
+/-- 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`. -/
+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 sub_one_norm.is_prime_pow (zeta_primitive_root n K L) hn hirr h,
+end
+
+/-- 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 {p : ℕ+} [ne_zero ((p : ℕ) : K)] (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 },
+  refine prime_ne_two_pow.sub_one_norm k (zeta_primitive_root _ K L) hirr h,
+end
+
+/-- 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 {p : ℕ+} [ne_zero ((p : ℕ) : K)] [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 sub_one_norm.prime (zeta_primitive_root _ K L) hirr h,
+end
+
+/-- 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)
+  [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.pow_two hk _ hirr,
+  simpa using zeta_primitive_root (2 ^ k) K L,
+end
+
+end is_cyclotomic_extension
+
+end norm