useless

leanprover-community · Jul 3, 2024 · 2e4d37d · 2e4d37d
1 parent a43940b
commit 2e4d37d
Show file tree

Hide file tree

Showing 2 changed files with 0 additions and 4 deletions.
diff --git a/FltRegular/CaseII/AuxLemmas.lean b/FltRegular/CaseII/AuxLemmas.lean
@@ -4,7 +4,6 @@ import FltRegular.NumberTheory.Cyclotomic.UnitLemmas
 import Mathlib.RingTheory.Ideal.Norm
 import Mathlib.RingTheory.ClassGroup
 import FltRegular.NumberTheory.Cyclotomic.MoreLemmas
-import FltRegular.ReadyForMathlib.PowerBasis
 
 variable {K : Type*} {p : ℕ+} [hpri : Fact p.Prime] [Field K] [CharZero K] [IsCyclotomicExtension {p} ℚ K]
 

diff --git a/FltRegular/ReadyForMathlib/PowerBasis.lean b/FltRegular/ReadyForMathlib/PowerBasis.lean
@@ -7,9 +7,6 @@ open RingOfIntegers Ideal Finset Nat FiniteDimensional
 
 variable {K : Type _} [Field K] (pb : PowerBasis ℤ (𝓞 K))
 
-instance instModuleSubtypeMemSubalgebraIntRingOfIntegers_fltRegular_bis :
-    Module (𝓞 K) (𝓞 K) := Semiring.toModule
-
 theorem exists_int_sModEq (x : 𝓞 K) :
     ∃ (n : ℤ), SModEq (span ({ pb.gen } : Set (𝓞 K))) x n := by
   refine' ⟨(pb.basis.repr x) ⟨0, pb.dim_pos⟩, _⟩