of_nat_of_neg — Mathlib

English

If both half-series converge multiplicably, then the full bilateral product converges multiplicably.

Русский

Если обе половины суммирования сходятся, то двустороннее произведение сходится.

LaTeX

$$$\\displaystyle \\text{Multipliable}((n\\mapsto f(n))) \\land \\text{Multipliable}((n\\mapsto f(-n))) \\Rightarrow \\text{Multipliable}(f)$$$

Lean4

@[to_additive]
theorem of_nat_of_neg {f : ℤ → G} (hf₁ : Multipliable fun n : ℕ ↦ f n) (hf₂ : Multipliable fun n : ℕ ↦ f (-n)) :
    Multipliable f :=
  (hf₁.hasProd.of_nat_of_neg hf₂.hasProd).multipliable

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