tprod_of_nat_of_neg_add_one — Mathlib

English

For multipliable f,g: ℕ→M, the infinite product over ℤ of Int.rec f g equals the product over ℕ of f times the product over ℕ of g.

Русский

Для мультиплируемых f,g: ℕ→M, бесконечное произведение по ℤ от Int.rec f g равно произведению f и произведению g по ℕ.

LaTeX

$$$\prod'_{n\in\mathbb{Z}} \text{Int.rec}(f,g)(n) = (\prod'_{n\in\mathbb{N}} f(n)) \cdot (\prod'_{n\in\mathbb{N}} g(n))$$$

Lean4

@[to_additive tsum_of_nat_of_neg_add_one]
theorem tprod_of_nat_of_neg_add_one [T2Space M] {f : ℤ → M} (hf₁ : Multipliable fun n : ℕ ↦ f n)
    (hf₂ : Multipliable fun n : ℕ ↦ f (-(n + 1))) : ∏' n : ℤ, f n = (∏' n : ℕ, f n) * ∏' n : ℕ, f (-(n + 1)) :=
  (hf₁.hasProd.of_nat_of_neg_add_one hf₂.hasProd).tprod_eq

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