linearCombination_single — Mathlib

English

For any a ∈ α and c ∈ R, linearCombination_R(v)(single a c) = c • v(a).

Русский

Для любых $a∈α$ и $c∈R$ линейная комбинация даёт $\text{linearCombination}_R(v)(\text{single }a c) = c \cdot v(a)$.

LaTeX

$$$\operatorname{linearCombination}_R(v)(\text{single } a\, c) = c \cdot v(a).$$$

Lean4

@[simp]
theorem linearCombination_single (c : R) (a : α) : linearCombination R v (single a c) = c • v a := by
  simp [linearCombination_apply, sum_single_index]

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