From 5728fdab8866cb6c5867e524bf0fdd13fce2a8de Mon Sep 17 00:00:00 2001 From: Riccardo Brasca Date: Wed, 3 Jul 2024 14:25:22 +0200 Subject: [PATCH] another one --- FltRegular/NumberTheory/CyclotomicRing.lean | 3 --- 1 file changed, 3 deletions(-) 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]