tprod_zero_pnat_eq_tprod_nat — Mathlib

English

If f is Multipliable, then f(0) times the tprod over positive naturals equals the tprod over all naturals.

Русский

Если f сумма применима, то f(0) умножает tprod по положительным нормально равно tprod по всем натуральным.

LaTeX

$$$\\displaystyle f(0) \\cdot \\prod'_{n:\\mathbb{N}^+} f(n) = \\prod'_{n:\\mathbb{N}} f(n)$$$

Lean4

@[to_additive]
theorem tprod_zero_pnat_eq_tprod_nat [TopologicalSpace G] [IsTopologicalGroup G] [T2Space G] {f : ℕ → G}
    (hf : Multipliable f) : f 0 * ∏' n : ℕ+, f ↑n = ∏' n, f n := by
  simpa [hf.tprod_eq_zero_mul] using tprod_pnat_eq_tprod_succ

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