coeFn_smul — Mathlib

English

Let f be an alternating R-linear map from M^ι to N. Then for every scalar c in S, the action of c on f corresponds to multiplying the values of f by c: (c • f)(v) = c • f(v) for all v ∈ ι → M.

Русский

Пусть f — чередующее R-линейное отображение из M^ι в N. Тогда для каждого скаляра c из S действие над f эквивалентно умножению значений отображения на c: (c • f)(v) = c • f(v) для всех v ∈ ι → M.

LaTeX

$$$\forall c \in S,\ \forall f \in \operatorname{AlternatingMap}(R,M,N,\iota),\ \forall v:\iota \to M,\ (c \cdot f)(v) = c \cdot f(v).$$$

Lean4

theorem coeFn_smul (c : S) (f : M [⋀^ι]→ₗ[R] N) : ⇑(c • f) = c • ⇑f :=
  rfl

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