tprod_of_nat_of_neg — Mathlib

English

If both halves are Multipliable, then the bilateral tprod equals the quotient of the product of nonnegative and negative parts by f(0).

Русский

Если обе половины произведения допустимы, то двусторонний т-произведение равно частному от произведения по неотрицательным и по отрицательным индексам на f(0).

LaTeX

$$$\\displaystyle \\text{tprod}_{n\\in\\mathbb{Z}} f(n) = \\dfrac{\\left(\\prod_{n\\ge 0} f(n)\\right) \\left(\\prod_{n\\ge 0} f(-n)\\right)}{f(0)}$$$

Lean4

@[to_additive]
protected theorem tprod_of_nat_of_neg [T2Space G] {f : ℤ → G} (hf₁ : Multipliable fun n : ℕ ↦ f n)
    (hf₂ : Multipliable fun n : ℕ ↦ f (-n)) : ∏' n : ℤ, f n = (∏' n : ℕ, f n) * (∏' n : ℕ, f (-n)) / f 0 :=
  (hf₁.hasProd.of_nat_of_neg hf₂.hasProd).tprod_eq

Похожие утверждения