sum_single_smul — Mathlib

English

Let f: ι → A and r ∈ R, i0 ∈ ι. Then the sum over i of the single i0 indicator times r acting on f(i) equals r · f(i0).

Русский

Пусть f: ι → α, r ∈ R, i0 ∈ ι. Тогда сумма по i от единицы в Pi для i0: (Pi.single i0 r i) • f(i) суммируется и равна r • f(i0).

LaTeX

$$$$ \\sum_i (\\Pi.single_{i_0} r i) \\cdot f(i) = r \\cdot f(i_0). $$$$

Lean4

@[simp]
theorem sum_single_smul {R : Type*} [Semiring R] [Module R α] (f : ι → α) (r : R) (i₀ : ι) :
    ∑ i, (Pi.single (M := fun _ ↦ R) i₀ r i) • f i = r • f i₀ := by
  rw [Finset.sum_eq_single i₀, Pi.single_eq_same] <;> aesop

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