remove bad instances

leanprover-community · Nov 27, 2023 · a9ecd67 · a9ecd67
1 parent 95ab3a5
commit a9ecd67
Show file tree

Hide file tree

Showing 5 changed files with 19 additions and 10 deletions.
diff --git a/FltRegular/NumberTheory/AuxLemmas.lean b/FltRegular/NumberTheory/AuxLemmas.lean
@@ -475,16 +475,16 @@ lemma inv_le_comm (hI : I ≠ 0) (hJ : J ≠ 0) : I⁻¹ ≤ J ↔ J⁻¹ ≤ I
 
 end FractionalIdeal
 
--- Mathlib/RingTheory/Localization/FractionRing.lean
-noncomputable
-instance {A B} [CommRing A] [CommRing B] [Algebra A B] [IsDomain A] [IsDomain B]
-    [NoZeroSMulDivisors A B] : Algebra (FractionRing A) (FractionRing B) :=
-  FractionRing.liftAlgebra A _
-
--- Mathlib/RingTheory/Localization/FractionRing.lean
-instance {A B} [CommRing A] [CommRing B] [Algebra A B] [IsDomain A] [IsDomain B]
-    [NoZeroSMulDivisors A B] : IsScalarTower A (FractionRing A) (FractionRing B) :=
-  FractionRing.isScalarTower_liftAlgebra _ _
+-- -- Mathlib/RingTheory/Localization/FractionRing.lean
+-- noncomputable
+-- instance {A B} [CommRing A] [CommRing B] [Algebra A B] [IsDomain A] [IsDomain B]
+--     [NoZeroSMulDivisors A B] : Algebra (FractionRing A) (FractionRing B) :=
+--   FractionRing.liftAlgebra A _
+
+-- -- Mathlib/RingTheory/Localization/FractionRing.lean
+-- instance {A B} [CommRing A] [CommRing B] [Algebra A B] [IsDomain A] [IsDomain B]
+--     [NoZeroSMulDivisors A B] : IsScalarTower A (FractionRing A) (FractionRing B) :=
+--   FractionRing.isScalarTower_liftAlgebra _ _
 
 open nonZeroDivisors
 section

diff --git a/FltRegular/NumberTheory/Different.lean b/FltRegular/NumberTheory/Different.lean
@@ -25,6 +25,8 @@ import Mathlib.NumberTheory.KummerDedekind
 -/
 universe u
 
+attribute [local instance] FractionRing.liftAlgebra FractionRing.isScalarTower_liftAlgebra
+
 variable (A K) {B} {L : Type u} [CommRing A] [Field K] [CommRing B] [Field L]
 variable [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L]
 variable [IsScalarTower A K L] [IsScalarTower A B L]

diff --git a/FltRegular/NumberTheory/IdealNorm.lean b/FltRegular/NumberTheory/IdealNorm.lean
@@ -14,6 +14,8 @@ Generalizes `Ideal.spanNorm` in `Mathlib/RingTheory/Ideal/Norm.lean` to non-free
 -/
 open scoped nonZeroDivisors
 
+attribute [local instance] FractionRing.liftAlgebra FractionRing.isScalarTower_liftAlgebra
+
 section intNorm
 
 universe u v w

diff --git a/FltRegular/NumberTheory/QuotientTrace.lean b/FltRegular/NumberTheory/QuotientTrace.lean
@@ -15,6 +15,9 @@ import FltRegular.NumberTheory.AuxLemmas
   The trace map on `B → A` coincides with the trace map on `B⧸pB → A⧸p`.
 
 -/
+
+attribute [local instance] FractionRing.liftAlgebra FractionRing.isScalarTower_liftAlgebra
+
 section LocalRing
 
 variable {R S} [CommRing R] [CommRing S] [Algebra R S] [LocalRing R] [Module.Free R S] [Module.Finite R S]

diff --git a/FltRegular/NumberTheory/Unramified.lean b/FltRegular/NumberTheory/Unramified.lean
@@ -19,6 +19,8 @@ import FltRegular.NumberTheory.Different
 -/
 open BigOperators UniqueFactorizationMonoid
 
+attribute [local instance] FractionRing.liftAlgebra FractionRing.isScalarTower_liftAlgebra
+
 variable (R K S L : Type*) [CommRing R] [CommRing S] [Algebra R S] [Field K] [Field L]
     [IsDedekindDomain R] [Algebra R K] [IsFractionRing R K] [Algebra S L] -- [IsFractionRing S L]
     [Algebra K L] [Algebra R L] [IsScalarTower R S L] [IsScalarTower R K L] -- [IsNoetherian R S]