sum — Mathlib

English

Summation over a finite set of terms is defined by a finite sum; the definable sum of f(i) over i ∈ s matches the term for sum s f.

Русский

Суммирование по конечному набору термов определяется через конечную сумму; сумма f(i) по i∈s равна терму суммы s f.

LaTeX

$$$ \\text{sum}(s,f) = \\sum_{i \\in s} f(i) $$$

Lean4

/-- Summation over a finite set of terms in Presburger arithmetic.

It is defined via choice, so the result only makes sense when the structure satisfies
commutativity (see `realize_sum`). -/
noncomputable def sum {β : Type*} (s : Finset β) (f : β → presburger.Term α) : presburger.Term α :=
  (s.toList.map f).sum

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