smul_sum — Mathlib

English

Scalar multiplication distributes over the sum: c • f.sum h = f.sum (λ a b, c • h a b).

Русский

Умножение скаляром распределяется по сумме: c • f.sum h = f.sum (λ a b, c • h a b).

LaTeX

$$$c \\cdot f.sum h = f.sum (\\\\lambda a b . c \\\\cdot h a b)$$$

Lean4

theorem smul_sum {α : Type*} [∀ i, Zero (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)] [AddCommMonoid γ] [DistribSMul α γ]
    {f : Π₀ i, β i} {h : ∀ i, β i → γ} {c : α} : c • f.sum h = f.sum fun a b => c • h a b :=
  Finset.smul_sum

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