toSpanSingleton_smul — Mathlib

English

Composition with toSpanSingleton respects evaluation: f ∘ toSpanSingleton x = toSpanSingleton (f x).

Русский

Составление с toSpanSingleton сохраняет применение: f ∘ toSpanSingleton x = toSpanSingleton (f x).

LaTeX

$$$ f \circ_L toSpanSingleton(R_1, x) = toSpanSingleton(R_1, f x).$$$

Lean4

theorem toSpanSingleton_smul {α} [Monoid α] [DistribMulAction α M₁] [ContinuousConstSMul α M₁] [SMulCommClass R₁ α M₁]
    (c : α) (x : M₁) : toSpanSingleton R₁ (c • x) = c • toSpanSingleton R₁ x :=
  coe_inj.mp <| LinearMap.toSpanSingleton_smul _ _

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