English
For any f: Fin(n+1) → M, the full product equals f(0) times the product of f over the successors of indices in Fin n.
Русский
Для любого f: Fin(n+1) → M всякое полное произведение равно f(0), умноженному на произведение f над последовательными индексами в Fin n.
LaTeX
$$$\displaystyle \prod_{i \in \mathrm{Fin}(n+1)} f(i) = f(0) \cdot \prod_{i \in \mathrm{Fin}(n)} f(i.\mathrm{succ}).$$$
Lean4
/-- A product of a function `f : Fin (n + 1) → M` over all `Fin (n + 1)`
is the product of `f 0` times the remaining product -/
@[to_additive /-- A sum of a function `f : Fin (n + 1) → M` over all `Fin (n + 1)` is the sum of
`f 0` plus the remaining sum -/
]
theorem prod_univ_succ (f : Fin (n + 1) → M) : ∏ i, f i = f 0 * ∏ i : Fin n, f i.succ :=
prod_univ_succAbove f 0
