diff --git a/Mathlib/NumberTheory/Cyclotomic/Rat.lean b/Mathlib/NumberTheory/Cyclotomic/Rat.lean
index 8819be702853b..ff9183d9b9fb2 100644
--- a/Mathlib/NumberTheory/Cyclotomic/Rat.lean
+++ b/Mathlib/NumberTheory/Cyclotomic/Rat.lean
@@ -5,6 +5,7 @@ Authors: Riccardo Brasca
 -/
 import Mathlib.NumberTheory.Cyclotomic.Discriminant
 import Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
+import Mathlib.RingTheory.Ideal.Norm
 
 #align_import number_theory.cyclotomic.rat from "leanprover-community/mathlib"@"b353176c24d96c23f0ce1cc63efc3f55019702d9"
 
@@ -181,11 +182,14 @@ noncomputable def integralPowerBasis [IsCyclotomicExtension {p ^ k} ℚ K]
   (Algebra.adjoin.powerBasis' (hζ.isIntegral (p ^ k).pos)).map hζ.adjoinEquivRingOfIntegers
 #align is_primitive_root.integral_power_basis IsPrimitiveRoot.integralPowerBasis
 
+/-- Abbreviation to see a primitive root of unity as a member of the ring of integers. -/
+abbrev toInteger {k : ℕ+} (hζ : IsPrimitiveRoot ζ k) : 𝓞 K := ⟨ζ, hζ.isIntegral k.pos⟩
+
 --Porting note: the proof changed because `simp` unfolds too much.
 @[simp]
 theorem integralPowerBasis_gen [hcycl : IsCyclotomicExtension {p ^ k} ℚ K]
     (hζ : IsPrimitiveRoot ζ ↑(p ^ k)) :
-    hζ.integralPowerBasis.gen = ⟨ζ, hζ.isIntegral (p ^ k).pos⟩ :=
+    hζ.integralPowerBasis.gen = hζ.toInteger :=
   Subtype.ext <| show algebraMap _ K hζ.integralPowerBasis.gen = _ by
     rw [integralPowerBasis, PowerBasis.map_gen, adjoin.powerBasis'_gen]
     simp only [adjoinEquivRingOfIntegers_apply, IsIntegralClosure.algebraMap_lift]
@@ -223,7 +227,7 @@ noncomputable def integralPowerBasis' [hcycl : IsCyclotomicExtension {p} ℚ K]
 
 @[simp]
 theorem integralPowerBasis'_gen [hcycl : IsCyclotomicExtension {p} ℚ K] (hζ : IsPrimitiveRoot ζ p) :
-    hζ.integralPowerBasis'.gen = ⟨ζ, hζ.isIntegral p.pos⟩ :=
+    hζ.integralPowerBasis'.gen = hζ.toInteger :=
   @integralPowerBasis_gen p 1 K _ _ _ _ (by convert hcycl; rw [pow_one]) (by rwa [pow_one])
 #align is_primitive_root.integral_power_basis'_gen IsPrimitiveRoot.integralPowerBasis'_gen
 
@@ -242,7 +246,7 @@ noncomputable def subOneIntegralPowerBasis [IsCyclotomicExtension {p ^ k} ℚ K]
     (isIntegral_of_mem_ringOfIntegers <|
       Subalgebra.sub_mem _ (hζ.isIntegral (p ^ k).pos) (Subalgebra.one_mem _))
     (by
-      simp only [integralPowerBasis_gen]
+      simp only [integralPowerBasis_gen, toInteger]
       convert Subalgebra.add_mem _ (self_mem_adjoin_singleton ℤ (⟨ζ - 1, _⟩ : 𝓞 K))
         (Subalgebra.one_mem _)
 -- Porting note: `simp` was able to finish the proof.
@@ -269,11 +273,77 @@ noncomputable def subOneIntegralPowerBasis' [hcycl : IsCyclotomicExtension {p} 
 @[simp]
 theorem subOneIntegralPowerBasis'_gen [hcycl : IsCyclotomicExtension {p} ℚ K]
     (hζ : IsPrimitiveRoot ζ p) :
-    hζ.subOneIntegralPowerBasis'.gen =
-      ⟨ζ - 1, Subalgebra.sub_mem _ (hζ.isIntegral p.pos) (Subalgebra.one_mem _)⟩ :=
+    hζ.subOneIntegralPowerBasis'.gen = hζ.toInteger - 1 :=
   @subOneIntegralPowerBasis_gen p 1 K _ _ _ _ (by convert hcycl; rw [pow_one]) (by rwa [pow_one])
 #align is_primitive_root.sub_one_integral_power_basis'_gen IsPrimitiveRoot.subOneIntegralPowerBasis'_gen
 
+/-- `ζ - 1` is prime if `p ≠ 2` and `ζ` is a primitive `p ^ (k + 1)`-th root of unity.
+  See `zeta_sub_one_prime` for a general statement. -/
+theorem zeta_sub_one_prime_of_ne_two [IsCyclotomicExtension {p ^ (k + 1)} ℚ K]
+    (hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))) (hodd : p ≠ 2) :
+    Prime (hζ.toInteger - 1) := by
+  letI := IsCyclotomicExtension.numberField {p ^ (k + 1)} ℚ K
+  refine Ideal.prime_of_irreducible_absNorm_span (fun h ↦ ?_) ?_
+  · apply hζ.pow_ne_one_of_pos_of_lt zero_lt_one (one_lt_pow hp.out.one_lt (by simp))
+    rw [← Subalgebra.coe_eq_zero] at h
+    simpa [sub_eq_zero] using h
+  rw [Nat.irreducible_iff_prime, Ideal.absNorm_span_singleton, ← Nat.prime_iff,
+    ← Int.prime_iff_natAbs_prime]
+  convert Nat.prime_iff_prime_int.1 hp.out
+  apply RingHom.injective_int (algebraMap ℤ ℚ)
+  rw [← Algebra.norm_localization (Sₘ := K) ℤ (nonZeroDivisors ℤ), Subalgebra.algebraMap_eq]
+  simp only [PNat.pow_coe, id.map_eq_id, RingHomCompTriple.comp_eq, RingHom.coe_coe,
+    Subalgebra.coe_val, algebraMap_int_eq, map_natCast]
+  exact hζ.sub_one_norm_prime_ne_two (Polynomial.cyclotomic.irreducible_rat (PNat.pos _)) hodd
+
+/-- `ζ - 1` is prime if `ζ` is a primitive `2 ^ (k + 1)`-th root of unity.
+  See `zeta_sub_one_prime` for a general statement. -/
+theorem zeta_sub_one_prime_of_two_pow [IsCyclotomicExtension {(2 : ℕ+) ^ (k + 1)} ℚ K]
+    (hζ : IsPrimitiveRoot ζ ↑((2 : ℕ+) ^ (k + 1))) :
+    Prime (hζ.toInteger - 1) := by
+  letI := IsCyclotomicExtension.numberField {(2 : ℕ+) ^ (k + 1)} ℚ K
+  refine Ideal.prime_of_irreducible_absNorm_span (fun h ↦ ?_) ?_
+  · apply hζ.pow_ne_one_of_pos_of_lt zero_lt_one (one_lt_pow (by norm_num) (by simp))
+    rw [← Subalgebra.coe_eq_zero] at h
+    simpa [sub_eq_zero] using h
+  rw [Nat.irreducible_iff_prime, Ideal.absNorm_span_singleton, ← Nat.prime_iff,
+    ← Int.prime_iff_natAbs_prime]
+  cases k
+  · convert Prime.neg Int.prime_two
+    apply RingHom.injective_int (algebraMap ℤ ℚ)
+    rw [← Algebra.norm_localization (Sₘ := K) ℤ (nonZeroDivisors ℤ), Subalgebra.algebraMap_eq]
+    simp only [Nat.zero_eq, PNat.pow_coe, id.map_eq_id, RingHomCompTriple.comp_eq, RingHom.coe_coe,
+      Subalgebra.coe_val, algebraMap_int_eq, map_neg, map_ofNat]
+    simpa using hζ.pow_sub_one_norm_two (cyclotomic.irreducible_rat (by simp))
+  convert Int.prime_two
+  apply RingHom.injective_int (algebraMap ℤ ℚ)
+  rw [← Algebra.norm_localization (Sₘ := K) ℤ (nonZeroDivisors ℤ), Subalgebra.algebraMap_eq]
+  simp only [PNat.pow_coe, id.map_eq_id, RingHomCompTriple.comp_eq, RingHom.coe_coe,
+    Subalgebra.coe_val, algebraMap_int_eq, map_natCast]
+  exact hζ.sub_one_norm_two Nat.AtLeastTwo.prop (cyclotomic.irreducible_rat (by simp))
+
+/-- `ζ - 1` is prime if `ζ` is a primitive `p ^ (k + 1)`-th root of unity. -/
+theorem zeta_sub_one_prime [IsCyclotomicExtension {p ^ (k + 1)} ℚ K]
+    (hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))) : Prime (hζ.toInteger - 1) := by
+  by_cases htwo : p = 2
+  · subst htwo
+    apply hζ.zeta_sub_one_prime_of_two_pow
+  · apply hζ.zeta_sub_one_prime_of_ne_two htwo
+
+/-- `ζ - 1` is prime if `ζ` is a primitive `p`-th root of unity. -/
+theorem zeta_sub_one_prime' [h : IsCyclotomicExtension {p} ℚ K] (hζ : IsPrimitiveRoot ζ p) :
+    Prime ((hζ.toInteger - 1)) := by
+  convert zeta_sub_one_prime (k := 0) (by simpa)
+  simpa
+
+theorem subOneIntegralPowerBasis_gen_prime [IsCyclotomicExtension {p ^ (k + 1)} ℚ K]
+    (hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))) :
+    Prime hζ.subOneIntegralPowerBasis.gen := by simpa using hζ.zeta_sub_one_prime
+
+theorem subOneIntegralPowerBasis'_gen_prime [IsCyclotomicExtension {p} ℚ K]
+    (hζ : IsPrimitiveRoot ζ ↑p) :
+    Prime hζ.subOneIntegralPowerBasis'.gen := by simpa using hζ.zeta_sub_one_prime'
+
 end IsPrimitiveRoot
 
 end PowerBasis