English
For any x in M and f: Fin(n) → M, the product over Fin(n+1) of the sequence obtained by prepending x to f equals x times the product of f over Fin(n).
Русский
Для любого x в M и функции f: Fin(n) → M произведение по Fin(n+1) последовательности, полученной путем добавления x в начало, равно x умножить на произведение f над Fin(n).
LaTeX
$$$\displaystyle \prod_{i \in \mathrm{Fin}(n+1)} (\mathrm{cons}(x,f))(i) = x \cdot \prod_{i \in \mathrm{Fin}(n)} f(i).$$$
Lean4
@[to_additive (attr := simp)]
theorem prod_cons (x : M) (f : Fin n → M) : (∏ i : Fin n.succ, (cons x f : Fin n.succ → M) i) = x * ∏ i : Fin n, f i :=
by simp_rw [prod_univ_succ, cons_zero, cons_succ]
