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 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