linearCombination_single_index — Mathlib

English

For any c ∈ M, a ∈ α, f ∈ α →₀ R, linearCombination_R(v)(Pi.single a c)(f) = f(a) • c.

Русский

Для любых $c∈M$, $a∈α$, $f∈α→₀R$ верно: линейная комбинация с $Pi.single a c$ на $f$ даёт $f(a)\,c$.

LaTeX

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

Lean4

@[simp]
theorem linearCombination_single_index (c : M) (a : α) (f : α →₀ R) [DecidableEq α] :
    linearCombination R (Pi.single a c) f = f a • c :=
  by
  rw [linearCombination_apply, sum_eq_single a, Pi.single_eq_same]
  · exact fun i _ hi ↦ by rw [Pi.single_eq_of_ne hi, smul_zero]
  · exact fun _ ↦ by simp only [zero_smul]

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