English
Define partialProd for a sequence f: Fin n → M by taking the product of the first i elements, i ranging over Fin(n+1). It is the product of all f(j) with j < i.
Русский
Определим partialProd для последовательности f: Fin n → M как произведение первых i элементов; i пробегает по Fin(n+1). Это произведение всех f(j) при j < i.
LaTeX
$$$$\\text{partialProd}(f, i) = \\left(\\text{List.ofFn}(f)\\right)_{0} \\cdots \\left(\\text{List.ofFn}(f)\\right)_{i-1}.$$$$
Lean4
/-- For `f = (a₁, ..., aₙ)` in `αⁿ`, `partialProd f` is `(1, a₁, a₁a₂, ..., a₁...aₙ)` in `αⁿ⁺¹`. -/
@[to_additive /-- For `f = (a₁, ..., aₙ)` in `αⁿ`, `partialSum f` is
`(0, a₁, a₁ + a₂, ..., a₁ + ... + aₙ)` in `αⁿ⁺¹`. -/
]
def partialProd (f : Fin n → M) (i : Fin (n + 1)) : M :=
((List.ofFn f).take i).prod
