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