sum_mul — Mathlib

English

Multiplication by a scalar on the outer side distributes over the sum: b · (s.sum f) = s.sum (λ a c, b · f a c).

Русский

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

LaTeX

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

Lean4

theorem sum_mul {S : Type*} [NonUnitalNonAssocSemiring S] (b : S) (s : SkewMonoidAlgebra k G) {f : G → k → S} :
    s.sum f * b = s.sum fun a c ↦ f a c * b := by simp only [sum, Finsupp.sum, Finset.sum_mul]

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