English
Let M be a topological commutative monoid with a continuous multiplication and T2-separation. If f: Z → M is multipliable (the bilateral infinite product converges), then the product over nonnegative indices of f(n) and f(−n) equals the bilateral product up to a factor f(0): ∏'_{n≥0} (f(n) f(−n)) = (∏'_{n∈Z} f(n)) · f(0).
Русский
Пусть M — топологическое коммутативное полугруппе с непрерывным умножением и T2-сепарабельностью. Если f: Z → M сходится в смысле двустороннего произведения (суммирование по произведениям сходится), то произведение по неотрицательным индексам с чередованием знаков равно двустороннему произведению, умноженному на f(0): ∏'_{n≥0} (f(n) f(−n)) = (∏'_{n∈Z} f(n)) · f(0).
LaTeX
$$$\\displaystyle \\prod\\limits_{n \\ge 0}' \\bigl(f(n) f(-n)\\bigr) = \\Bigl(\\prod\\limits_{n \\in \\mathbb{Z}} f(n)\\Bigr) \\cdot f(0)$$$
Lean4
@[to_additive]
theorem tprod_nat_mul_neg [T2Space M] {f : ℤ → M} (hf : Multipliable f) :
∏' n : ℕ, (f n * f (-n)) = (∏' n : ℤ, f n) * f 0 :=
hf.hasProd.nat_mul_neg.tprod_eq
