another one

leanprover-community · Jul 3, 2024 · 5728fda · 5728fda
1 parent 669b5af
commit 5728fda
Showing 1 changed file with 0 additions and 3 deletions.
diff --git 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]