English
If the positive-index product ∏_{n≥0} f(n+1) converges to m and the product over negative indices ∏_{n≥0} f(-(n+1)) converges to m', then the full bilateral product ∏_{n∈Z} f(n) converges to m f(0) m'.
Русский
Если произведение по неотрицательным индексам без первого элемента сходится к m, а по отрицательным индексам сходится к m', то двустороннее произведение сходится и равно m f(0) m'.
LaTeX
$$$\\displaystyle \\text{HasProd}\\ f\\ (m)\\ (f(n+1)) \\land \\text{HasProd}\\ f\\ (m')\\ (f(-(n+1))) \\Rightarrow \\text{HasProd}\\ f\\ (m \\cdot f(0) \\cdot m')$$$
Lean4
@[to_additive HasSum.of_add_one_of_neg_add_one]
theorem of_add_one_of_neg_add_one {f : ℤ → M} (hf₁ : HasProd (fun n : ℕ ↦ f (n + 1)) m)
(hf₂ : HasProd (fun n : ℕ ↦ f (-(n + 1))) m') : HasProd f (m * f 0 * m') :=
HasProd.of_nat_of_neg_add_one (mul_comm _ m ▸ HasProd.zero_mul hf₁) hf₂
