botContinuousSMul — Mathlib

English

Let K ⊆ L be a field extension and M an intermediate field. The natural scalar action of M on the bottom intermediate field ⊥ (viewed as a subfield of L) by multiplication is continuous.

Русский

Пусть K ⊆ L — расширение полей и M — промежуточное поле. Естественное скалярное действие M на нижнем промежуточном поле ⊥ (рассматриваемом как подполе L) по умножению непрерывно.

LaTeX

$$$\\mathrm{ContinuousSMul}\\left(\\perp,\\ M\\right)$$$

Lean4

instance botContinuousSMul (M : IntermediateField K L) : ContinuousSMul (⊥ : IntermediateField K L) M :=
  Topology.IsInducing.continuousSMul (X := L) (N := (⊥ : IntermediateField K L)) (Y := M) (M :=
    (⊥ : IntermediateField K L)) Topology.IsInducing.subtypeVal continuous_id rfl

Похожие утверждения