toSMul — Mathlib

English

Convert box-additive map to a scalar action-valued map. Each f maps I to a linear operator on E.

Русский

Преобразовать BoxAdditiveMap в отображение, задающее действие скаляра на E.

LaTeX

$$$f \mapsto f.toSMul$$$

Lean4

/-- If `f` is a box-additive map, then so is the map sending `I` to the scalar multiplication
by `f I` as a continuous linear map from `E` to itself. -/
def toSMul (f : ι →ᵇᵃ[I₀] ℝ) : ι →ᵇᵃ[I₀] E →L[ℝ] E :=
  f.map (ContinuousLinearMap.lsmul ℝ ℝ).toLinearMap.toAddMonoidHom

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