restrictScalarsₗ — Mathlib

English

There is a canonical linear map from ContinuousLinearMap to LinearMap that respects scalar towers A → R → S.

Русский

Существует каноническое линейное отображение, совместимое с цепочкой скаляров A → R → S.

LaTeX

$$$$ \text{restrictScalarsₗ}(f) : M \toL[R] M_2 \quad \text{is a } S\text{-linear map}. $$$$

Lean4

/-- `ContinuousLinearMap.restrictScalars` as a `LinearMap`. See also
`ContinuousLinearMap.restrictScalarsL`. -/
def restrictScalarsₗ : (M₁ →L[A] M₂) →ₗ[S] M₁ →L[R] M₂
    where
  toFun := restrictScalars R
  map_add' := restrictScalars_add
  map_smul' := restrictScalars_smul

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