sum_single_index — Mathlib

English

Let N be a commutative additive monoid. For any a ∈ G and b ∈ k, and h: G × k → N with h(a,0) = 0, we have (single a b).sum h = h(a,b).

Русский

Пусть N — коммутативная аддитивная моноид; для любого a ∈ G, b ∈ k и h: G×k → N с h(a,0)=0 выполнено: (single a b).sum h = h(a,b).

LaTeX

$$$\\mathrm{single}(a,b).\\mathrm{sum}\\ h = h(a,b)$$$

Lean4

@[simp]
theorem sum_single_index {N} [AddCommMonoid N] {a : G} {b : k} {h : G → k → N} (h_zero : h a 0 = 0) :
    (SkewMonoidAlgebra.single a b).sum h = h a b :=
  Finsupp.sum_single_index h_zero

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