diff --git a/FltRegular/NumberTheory/CyclotomicRing.lean b/FltRegular/NumberTheory/CyclotomicRing.lean
index 7293fe50..63510e7c 100644
--- a/FltRegular/NumberTheory/CyclotomicRing.lean
+++ b/FltRegular/NumberTheory/CyclotomicRing.lean
@@ -100,9 +100,6 @@ lemma exists_dvd_int (n : CyclotomicIntegers p) (hn : n ≠ 0) : ∃ m : ℤ, m
 def powerBasis : PowerBasis ℤ (CyclotomicIntegers p) :=
    AdjoinRoot.powerBasis' (cyclotomic.monic _ _)
 
-@[simp]
-lemma powerBasis_gen : (powerBasis p).gen = zeta p := rfl
-
 lemma powerBasis_dim : (powerBasis p).dim = p - 1 := by
   simp [powerBasis, Nat.totient_prime hpri.out, natDegree_cyclotomic]