English
Let α be a type with addition and zero. For each m ≥ 0, define S_m : (Fin m → α) → α by S_0 = 0, S_1(v) = v(0), and for m ≥ 0, S_{m+2}(v) = S_m(v ∘ shift) + v(last). Equivalently, S_m recursively aggregates the m entries of v by folding with + starting from 0.
Русский
Пусть α — множество с операциями сложения и нулём. Пусть для каждого натурального m задать S_m: (Fin m → α) → α по определению: S_0 = 0, S_1(v) = v(0), а для m ≥ 0 S_{m+2}(v) = S_m(v ∘ сдвиг) + v(last). То есть S_m задаёт сумму m элементов вектора v путём рекурсивного сложения.
LaTeX
$$$S_0 = 0,\\quad S_1(v) = v(0),\\quad S_{m+2}(v_0,\\dots,v_{m+1}) = S_m(v_1,\\dots,v_{m+1}) + v_{m+1}.$$$
Lean4
/-- `Finset.univ.sum` with better defeq for `Fin`. -/
def sum [Add α] [Zero α] : ∀ {m} (_ : Fin m → α), α
| 0, _ => 0
| 1, v => v 0
| _ + 2, v =>
sum (fun i => v (Fin.castSucc i)) +
v
(Fin.last _)
-- `to_additive` without `existing` fails, see
-- https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/to_additive.20complains.20about.20equation.20lemmas/near/508910537
