From fa5a1b2f26de020166d01a88ce74a08da0611708 Mon Sep 17 00:00:00 2001
From: jjdishere <emailboxofjjd@163.com>
Date: Wed, 23 Oct 2024 19:03:33 +0200
Subject: [PATCH] Reapply "ContinuousSMul for subfield intermediate fields"

This reverts commit ff465bfe7fa7c368063fc47f0666c75337c89935.
---
 Mathlib/Topology/Algebra/Algebra.lean    |  4 ++++
 Mathlib/Topology/Algebra/Field.lean      | 26 +++++++++++++++++++++++-
 Mathlib/Topology/Algebra/Ring/Basic.lean |  8 ++++++++
 3 files changed, 37 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Topology/Algebra/Algebra.lean b/Mathlib/Topology/Algebra/Algebra.lean
index 367ba0a65e42e..c3a600fb1ad0b 100644
--- a/Mathlib/Topology/Algebra/Algebra.lean
+++ b/Mathlib/Topology/Algebra/Algebra.lean
@@ -52,6 +52,10 @@ 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
index c897f0bb8fa18..9e6b964c7d50a 100644
--- 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.Algebra.Field.Subfield
+import Mathlib.FieldTheory.Adjoin
 import Mathlib.Algebra.GroupWithZero.Divisibility
 import Mathlib.Topology.Algebra.GroupWithZero
 import Mathlib.Topology.Algebra.Ring.Basic
@@ -149,3 +149,27 @@ 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 {F : Type*} [DivisionRing F] [TopologicalSpace F] [TopologicalRing F]
+
+variable {K L : Type*} [Field K] [Field L] [Algebra K L]
+    [TopologicalSpace L] [TopologicalRing L]
+
+variable (X : Type*) [TopologicalSpace X]
+    [MulAction L X] [ContinuousSMul L X]
+    [MulAction F X] [ContinuousSMul F X]
+
+instance Subfield.continuousSMul (M : Subfield F) : ContinuousSMul M X :=
+  Subring.continuousSMul M.toSubring X
+
+instance IntermediateField.continuousSMul (M : IntermediateField K L) : ContinuousSMul M X :=
+  M.toSubfield.continuousSMul X
+
+instance IntermediateField.botContinuousSMul (M : IntermediateField K L) :
+    ContinuousSMul (⊥ : IntermediateField K L) M :=
+  Inducing.continuousSMul (X := L) (N := (⊥ : IntermediateField K L)) (Y := M)
+    (M := (⊥ : IntermediateField K L)) inducing_subtype_val continuous_id rfl
+
+end ContinuousSMul
diff --git a/Mathlib/Topology/Algebra/Ring/Basic.lean b/Mathlib/Topology/Algebra/Ring/Basic.lean
index 94cf82277f373..f1f37c1d67625 100644
--- a/Mathlib/Topology/Algebra/Ring/Basic.lean
+++ b/Mathlib/Topology/Algebra/Ring/Basic.lean
@@ -91,6 +91,10 @@ 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
@@ -234,6 +238,10 @@ 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 α :=