linearCombination_unique — Mathlib

English

Same as above: linearCombination_unique expresses the same equality with Unique α as l default • v default.

Русский

То же самое: линейная комбинация равна произведению коэффициента по умолчанию на вектор по умолчанию.

LaTeX

$$$\operatorname{linearCombination}_R(v)(l) = l\,\text{default} \cdot v\,\text{default}$.$$

Lean4

theorem linearCombination_unique [Unique α] (l : α →₀ R) (v : α → M) :
    linearCombination R v l = l default • v default := by rw [← linearCombination_single, ← unique_single l]

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