prod_snoc — Mathlib

English

Let f: Fin(n+1) → M. The product over Fin(n+1) can be written as the product over Fin n of f(castSucc i) multiplied by f(last n).

Русский

Пусть 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

@[to_additive (attr := simp)]
theorem prod_snoc (x : M) (f : Fin n → M) :
    (∏ i : Fin n.succ, (snoc f x : Fin n.succ → M) i) = (∏ i : Fin n, f i) * x := by simp [prod_univ_castSucc]

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