restrictScalarsCLM — Mathlib

English

The operator that restricts scalars and then includes into CLM is continuous and compatible with the existing linear structure.

Русский

Оператор ограничения скаляров с последующим включением в CLM непрерывен и согласуется с линейной структурой.

LaTeX

$$$\\text{restrictScalars} \\text{ followed by CLM inclusion is continuous}$$$

Lean4

/-- `ContinuousMultilinearMap.restrictScalars` as a `ContinuousLinearMap`. -/
@[simps -fullyApplied apply]
def restrictScalarsCLM [ContinuousConstSMul 𝕜' F] : E [⋀^ι]→L[𝕜] F →L[𝕜'] E [⋀^ι]→L[𝕜'] F
    where
  toFun := restrictScalars 𝕜'
  map_add' _ _ := rfl
  map_smul' _ _ := rfl

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