English
Let f: Fin(n+1) → M. The product over all Fin(n+1) equals the product over Fin(n) of f applied to the shifted indices, multiplied by f at the last index.
Русский
Пусть f: Fin(n+1) → M. Произведение по Fin(n+1) равно произведению по Fin(n) от значений f(castSucc i), умноженного на f(last n).
LaTeX
$$$\displaystyle \prod_{i \in \mathrm{Fin}(n+1)} f(i) = \left(\prod_{i \in \mathrm{Fin}(n)} f(\mathrm{castSucc}(i))\right) \cdot f(\mathrm{last}(n)).$$$
Lean4
/-- A product of a function `f : Fin (n + 1) → M` over all `Fin (n + 1)`
is the product of `f (Fin.last n)` 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 (Fin.last n)` plus the remaining sum -/
]
theorem prod_univ_castSucc (f : Fin (n + 1) → M) : ∏ i, f i = (∏ i : Fin n, f (Fin.castSucc i)) * f (last n) := by
simpa [mul_comm] using prod_univ_succAbove f (last n)
