tprod_nat_mul_neg_add_one — Mathlib

English

For multipliable f: ℤ → M, the product over nonnegative integers of f(n) times f(−n−1) equals the product over all integers of f.

Русский

Для мультиплируемой f: ℤ → M произведение по неотрицательным целым числам f(n)·f(−n−1) равно произведению по всем целым числам f.

LaTeX

$$$\prod' n ∈ \mathbb{N}, (f(n) \cdot f(-n-1)) = \prod' n ∈ \mathbb{Z}, f(n)$$$

Lean4

@[to_additive tsum_nat_add_neg_add_one]
theorem tprod_nat_mul_neg_add_one [T2Space M] {f : ℤ → M} (hf : Multipliable f) :
    ∏' (n : ℕ), (f n * f (-(n + 1))) = ∏' (n : ℤ), f n :=
  hf.hasProd.nat_mul_neg_add_one.tprod_eq

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