Reapply "ContinuousSMul for subfield intermediate fields"

This reverts commit ff465bf.

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]
 

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

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 α :=