English
Let M be a commutative monoid and f: ℕ → M such that the tail product ∏' i, f(i+k) is defined for a given k whenever the tail beginning at k is multipliable. Then the finite prefix product ∏_{i=0}^{k-1} f(i) times the tail product ∏' i, f(i+k) equals the full product ∏' i, f(i).
Русский
Пусть M — коммутативный моноид и f: ℕ → M так, что произведение по хвосту ∏' i, f(i+k) задано для данного k, если хвост, начиная с k, определим. Тогда произведение первых k факторов ∏_{i=0}^{k-1} f(i) умноженное на хвостовое произведение ∏' i, f(i+k) равно полному произведению ∏' i, f(i).
LaTeX
$$$\left(\prod_{i \in \mathrm{range}(k)} f(i)\right) \cdot \prod_{i \in \mathbb{N}} f(i+k) =\; \prod_{i \in \mathbb{N}} f(i)$.$$
Lean4
@[to_additive]
protected theorem prod_mul_tprod_nat_mul' {f : ℕ → M} {k : ℕ} (h : Multipliable (fun n ↦ f (n + k))) :
((∏ i ∈ range k, f i) * ∏' i, f (i + k)) = ∏' i, f i :=
h.hasProd.prod_range_mul.tprod_eq.symm
