smul_sum — Mathlib

English

A scalar multiple commutes with the SkewMonoid sum: c • (v.sum h) = v.sum (λ a b, c • h a b).

Русский

Скалярное умножение переносится через сумму в SkewMonoidAlgebra: c • (v.sum h) = v.sum (λ a b, c • h a b).

LaTeX

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

Lean4

theorem smul_sum {M : Type*} {R : Type*} [AddCommMonoid M] [DistribSMul R M] {v : SkewMonoidAlgebra k G} {c : R}
    {h : G → k → M} : c • v.sum h = v.sum fun a b ↦ c • h a b :=
  Finsupp.smul_sum

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