continuousSMul — Mathlib

English

If M is an intermediate field between K and L, with L acting on a space X and X having a continuous L-action, then M inherits a continuous scalar action on X via restriction.

Русский

Если M — промежуточное поле между K и L, пространства X с непрерывным действием L на X, то M наследует непрерывное скалярное действие на X через ограничение.

LaTeX

$$$\text{ContinuousSMul}\ M\ X$$$

Lean4

instance continuousSMul (M : IntermediateField K L) : ContinuousSMul M X :=
  M.toSubfield.continuousSMul X

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