of_nat_of_neg_add_one — Mathlib

English

If HasProd for f and HasProd for g hold, then the combined integer-indexed sequence Int.rec f g has HasProd with product m·m'.

Русский

Если HasProd для f и для g выполняются, то последовательность Int.rec f g имеет HasProd с произведением m·m'.

LaTeX

$$$\text{HasProd}(\text{Int.rec } f g) = \text{HasProd}(f) \cdot \text{HasProd}(g)$$$

Lean4

@[to_additive Summable.of_nat_of_neg_add_one]
theorem of_nat_of_neg_add_one {f : ℤ → M} (hf₁ : Multipliable fun n : ℕ ↦ f n)
    (hf₂ : Multipliable fun n : ℕ ↦ f (-(n + 1))) : Multipliable f :=
  (hf₁.hasProd.of_nat_of_neg_add_one hf₂.hasProd).multipliable

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