sum_mul — Mathlib

English

For a semiring-like context (NonUnitalNonAssocSemiring), and a fixed b ∈ S, the identity b * (s.sum f) = s.sum (λ a c, b * f a c) holds.

Русский

В полукольце без единицы и без ассоциативности выполняется: b умножить на сумма по s f равно сумма по s от b умножить на f.

LaTeX

$$$b * s.sum f = s.sum (\lambda a c, b * f a c).$$$

Lean4

theorem sum_mul (b : S) (s : α →₀ R) {f : α → R → S} : s.sum f * b = s.sum fun a c => f a c * b := by
  simp only [Finsupp.sum, Finset.sum_mul]

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