English
For f: Z→G, Multipliable f iff both f on nonnegative and f on negated shifted indices are Multipliable: (Multipliable f) ↔ (Multipliable f|ℕ) ∧ (Multipliable f|−(n+1)).
Русский
Для f: Z→G, умножимость эквивалентна тому, что сумма по неотрицательным индексам и по отрицательным сдвинутым индексам сходятся: Multipliable f ⇔ (Multipliable f(n)) и (Multipliable f(−(n+1))).
LaTeX
$$$\\displaystyle \\text{Multipliable}(f) \\iff \\bigl(\\text{Multipliable}(n\\mapsto f(n)) \\land \\text{Multipliable}(n\\mapsto f(-(n+1)))\\bigr)$$$
Lean4
/-- "iff" version of `Multipliable.of_nat_of_neg_add_one`. -/
@[to_additive /-- "iff" version of `Summable.of_nat_of_neg_add_one`. -/
]
theorem multipliable_int_iff_multipliable_nat_and_neg_add_one {f : ℤ → G} :
Multipliable f ↔ (Multipliable fun n : ℕ ↦ f n) ∧ (Multipliable fun n : ℕ ↦ f (-(n + 1))) :=
by
refine ⟨fun p ↦ ⟨?_, ?_⟩, fun ⟨hf₁, hf₂⟩ ↦ Multipliable.of_nat_of_neg_add_one hf₁ hf₂⟩ <;> apply p.comp_injective
exacts [Nat.cast_injective, @Int.negSucc.inj]
