smulRightₗ — Mathlib

English

There is a canonical coercion from ContinuousLinearMap to a corresponding LinearMap with a RingHom component σ₁₃.

Русский

Существует каноническое преобразование из ContinuousLinearMap в соответствующее LinearMap с компонентой кольцевого гомоморфизма σ₁₃.

LaTeX

$$$$ \text{coeLMₛₗ}(f) : \; \text{LinearMap} \; (σ_{13}) (M, M_3) $$$$

Lean4

/-- Given `c : E →L[R] S`, `c.smulRightₗ` is the linear map from `F` to `E →L[R] F`
sending `f` to `fun e => c e • f`. See also `ContinuousLinearMap.smulRightL`. -/
def smulRightₗ (c : M →L[R] S) : M₂ →ₗ[T] M →L[R] M₂
    where
  toFun := c.smulRight
  map_add' x
    y := by
    ext e
    apply smul_add (c e)
  map_smul' a
    x := by
    ext e
    dsimp
    apply smul_comm

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