smulRight — Mathlib

English

smulRight(c, f) is the map x ↦ c(x) • f, i.e., tensoring by M2.

Русский

smulRight(c, f) — это линейное отображение x ↦ c(x) · f, то есть тензорирование на M2.

LaTeX

$$$\text{smulRight}(c,f) : M_1 \to_L[R] M_2$ defined by $(\text{smulRight}(c,f))(x) = c(x) \cdot f$.$$

Lean4

/-- The linear map `fun x => c x • f`.  Associates to a scalar-valued linear map and an element of
`M₂` the `M₂`-valued linear map obtained by multiplying the two (a.k.a. tensoring by `M₂`).
See also `ContinuousLinearMap.smulRightₗ` and `ContinuousLinearMap.smulRightL`. -/
@[simps coe]
def smulRight (c : M₁ →L[R] S) (f : M₂) : M₁ →L[R] M₂ :=
  { c.toLinearMap.smulRight f with cont := c.2.smul continuous_const }

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