English
If the even-indexed tail ∏' k, f(2k) and the odd-indexed tail ∏' k, f(2k+1) are multipliable, then their products equal the full product ∏' k, f(k). In particular, the product over even indices times the product over odd indices equals the whole product.
Русский
Если хвост по чётным индексам ∏' k, f(2k) и хвост по нечётным индексам ∏' k, f(2k+1) определимы (multipliable), то их произведения равны полному произведению ∏' k, f(k).
LaTeX
$$$\bigl(\prod' k, f(2k)\bigr) \cdot \bigl(\prod' k, f(2k+1)\bigr) = \prod' k, f(k)$$$
Lean4
@[to_additive]
theorem tprod_even_mul_odd {f : ℕ → M} (he : Multipliable fun k ↦ f (2 * k)) (ho : Multipliable fun k ↦ f (2 * k + 1)) :
(∏' k, f (2 * k)) * ∏' k, f (2 * k + 1) = ∏' k, f k :=
(he.hasProd.even_mul_odd ho.hasProd).tprod_eq.symm
