Continuous actions related to intermediate fields

In this file we define the instances related to continuous actions of intermediate fields. The topology on intermediate fields is already defined in earlier file Mathlib/Topology/Algebra/Field.lean as the subspace topology.

instance IntermediateField.continuousSMul {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [TopologicalSpace L] (X : Type u_3) [TopologicalSpace X] [MulAction L X] [ContinuousSMul L X] (M : IntermediateField K L) : ContinuousSMul (↥M) X

instance IntermediateField.botContinuousSMul {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [TopologicalSpace L] [IsTopologicalRing L] (M : IntermediateField K L) : ContinuousSMul ↥⊥ ↥M