Revert "Merge branch 'jiedong_jiang_continuous_smul_intermediate_fiel…

…d' of https://github.com/leanprover-community/mathlib4 into jiedong_jiang_continuous_smul_intermediate_field" This reverts commit e3576a3, reversing changes made to ff465bf.
leanprover-community · Oct 23, 2024 · 8c75884 · 8c75884
1 parent e3576a3
commit 8c75884
Show file tree

Hide file tree

Showing 3 changed files with 1 addition and 37 deletions.
diff --git a/Mathlib/Topology/Algebra/Algebra.lean b/Mathlib/Topology/Algebra/Algebra.lean
@@ -52,10 +52,6 @@ theorem continuousSMul_of_algebraMap [TopologicalSemiring A] (h : Continuous (al
     ContinuousSMul R A :=
   ⟨(continuous_algebraMap_iff_smul R A).1 h⟩
 
-instance Subalgebra.continuousSMul (S : Subalgebra R A) (X) [TopologicalSpace X] [MulAction A X]
-    [ContinuousSMul A X] : ContinuousSMul S X :=
-  Subsemiring.continuousSMul S.toSubsemiring X
-
 section
 variable [ContinuousSMul R A]
 

diff --git a/Mathlib/Topology/Algebra/Field.lean b/Mathlib/Topology/Algebra/Field.lean
@@ -3,7 +3,7 @@ Copyright (c) 2021 Patrick Massot. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Patrick Massot, Kim Morrison
 -/
-import Mathlib.FieldTheory.IntermediateField.Basic
+import Mathlib.Algebra.Field.Subfield
 import Mathlib.Algebra.GroupWithZero.Divisibility
 import Mathlib.Topology.Algebra.GroupWithZero
 import Mathlib.Topology.Algebra.Ring.Basic
@@ -149,27 +149,3 @@ theorem IsPreconnected.eq_of_sq_eq [Field 𝕜] [HasContinuousInv₀ 𝕜] [Cont
       (iff_of_eq (iff_false _)).2 (hg_ne _)] at hy' ⊢ <;> assumption
 
 end Preconnected
-
-section ContinuousSMul
-
-variable {K L : Type*} [Field K] [Field L] [Algebra K L]
-    [TopologicalSpace L] [TopologicalRing L] (M : Subfield L)
-
-#synth SMul M L
-
-instance Subfield.continuousSMul (M : Subfield L) (X) [TopologicalSpace X] [MulAction L X]
-    [ContinuousSMul L X] : ContinuousSMul M X :=
-  Subsemiring.continuousSMul S.toSubsemiring X
-
-instance IntermediateField (M : IntermediateField K L)
-variable {K L : Type*} [Field K] [Field L] [Algebra K L]
-    [TopologicalSpace L] [TopologicalRing L] (M : IntermediateField K L) (N : Subalgebra K L)
-    (R : Subring L)
-
-#synth TopologicalSpace M
-#synth TopologicalSpace N
-#synth ContinuousSMul R L
-instance : ContinuousSMul N L := sorry
-#synth ContinuousSMul N L
-
-end ContinuousSMul
diff --git a/Mathlib/Topology/Algebra/Ring/Basic.lean b/Mathlib/Topology/Algebra/Ring/Basic.lean
@@ -91,10 +91,6 @@ namespace Subsemiring
 instance topologicalSemiring (S : Subsemiring α) : TopologicalSemiring S :=
   { S.toSubmonoid.continuousMul, S.toAddSubmonoid.continuousAdd with }
 
-instance continuousSMul (s : Subsemiring α) (X) [TopologicalSpace X] [MulAction α X]
-    [ContinuousSMul α X] : ContinuousSMul s X :=
-  Submonoid.continuousSMul
-
 end Subsemiring
 
 /-- The (topological-space) closure of a subsemiring of a topological semiring is
@@ -238,10 +234,6 @@ variable [Ring α] [TopologicalRing α]
 instance Subring.instTopologicalRing (S : Subring α) : TopologicalRing S :=
   { S.toSubmonoid.continuousMul, inferInstanceAs (TopologicalAddGroup S.toAddSubgroup) with }
 
-instance Subring.continuousSMul (s : Subring α) (X) [TopologicalSpace X] [MulAction α X]
-    [ContinuousSMul α X] : ContinuousSMul s X :=
-  Subsemiring.continuousSMul s.toSubsemiring X
-
 /-- The (topological-space) closure of a subring of a topological ring is
 itself a subring. -/
 def Subring.topologicalClosure (S : Subring α) : Subring α :=