smul_apply — Mathlib

English

Definition of the single map as a DistribMulActionSemiHom; it associates to each index a canonical inclusion map that respects scalar action.

Русский

Определение отображения single как DistribMulActionSemiHom; сопоставляет каждому индексу каноническое включение, сохраняющее действие скаляра.

LaTeX

$$single(a) : M →+[R] α →₀ M, с map_smul'$$

Lean4

theorem smul_apply [Zero M] [SMulZeroClass R M] (b : R) (v : α →₀ M) (a : α) : (b • v) a = b • v a :=
  rfl

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