English
If the tail block of length b of f on Fin(a+b) is identically 1, then the total product reduces to the product over Fin a with indices shifted by b.
Русский
Если хвостовая часть длины b функции f на Fin(a+b) равна единице, то произведение сводится к произведению по Fin a над смещёнными индексами на b.
LaTeX
$$$\displaystyle \prod_{i \in \mathrm{Fin}(a+b)} f(i) = \prod_{i \in \mathrm{Fin}(a)} f(\mathrm{castAdd}(b,i))\quad\text{если } f(\mathrm{natAdd}(a,j))=1 \text{ для всех } j\in\mathrm{Fin}(b).$$$
Lean4
@[to_additive]
theorem prod_trunc {a b : ℕ} (f : Fin (a + b) → M) (hf : ∀ j : Fin b, f (natAdd a j) = 1) :
(∏ i : Fin (a + b), f i) = ∏ i : Fin a, f (castAdd b i) := by rw [prod_univ_add, Fintype.prod_eq_one _ hf, mul_one]
