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