sum_single_index — Mathlib

English

Let h: M → R → N with h(m,0)=0. Then (single m r).sum h = h(m,r).

Русский

Пусть h: M → R → N удовлетворяет h(m,0)=0. Тогда (single m r).sum h = h(m,r).

LaTeX

$$$\\text{sum\_single\_index}\\ N (m:{\\!M}) (r:{\\!R}) (h: M \\to R \\to N)\\ (h\\_{zero}=0) : (single(m,r)).sum\\ h = h(m,r)$$$

Lean4

@[to_additive]
theorem sum_single_index [AddCommMonoid N] {m : M} {r : R} {h : M → R → N} (h_zero : h m 0 = 0) :
    (single m r).sum h = h m r := by simp [h_zero]

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