raise — Mathlib

English

raise produces the list of partial sums: raise [a1, a2, ...] n = [n + a1, n + a1 + a2, ...].

Русский

raise формирует цепь частичных сумм: raise [a1, a2, ...] n = [n + a1, n + a1 + a2, ...].

LaTeX

$$$\\operatorname{raise}([] , _) = [],\\quad \\operatorname{raise}(m::l, n) = (m+n) :: \\operatorname{raise}(l, m+n).$$$

Lean4

/-- Outputs the list of partial sums of the input list, that is
`raise [a₁, a₂, ...] n = [n + a₁, n + a₁ + a₂, ...]` -/
def raise : List ℕ → ℕ → List ℕ
  | [], _ => []
  | m :: l, n => (m + n) :: raise l (m + n)

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