English
For any f: Fin(n+1) → M and any x ∈ Fin(n+1), the product of f over all indices equals f(x) times the product of f over the remaining indices obtained by shifting with x.
Русский
Пусть f: Fin(n+1) → M и x ∈ Fin(n+1). Произведение по всем индексам равно f(x) умножить на произведение f над оставшимися индексами, получаемыми из x при помощи операции смещения.
LaTeX
$$$\displaystyle \prod_{i \in \mathrm{Fin}(n+1)} f(i) = f(x) \cdot \prod_{i \in \mathrm{Fin}(n)} f(x.\mathrm{succAbove}(i)).$$$
Lean4
/-- A product of a function `f : Fin (n + 1) → M` over all `Fin (n + 1)`
is the product of `f x`, for some `x : Fin (n + 1)` 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 x`, for some `x : Fin (n + 1)` plus the remaining sum -/
]
theorem prod_univ_succAbove (f : Fin (n + 1) → M) (x : Fin (n + 1)) : ∏ i, f i = f x * ∏ i : Fin n, f (x.succAbove i) :=
by rw [univ_succAbove n x, prod_cons, Finset.prod_map, coe_succAboveEmb]
