English
If HasProd for f on nonnegative indices with m and HasProd for the shifted negative part, then HasProd for the full ℤ-indexed sequence f with product m m'. The full product is the product of range-1 parts combined with the shifted part via the complement structure.
Русский
Если HasProd по неотрицательным индексам и HasProd по сдвинутым отрицательным частям, то HasProd для всей последовательности ℤ задаётся как произведение частей.
LaTeX
$$$\text{HasProd}(f) = \text{HasProd}(f\downarrow\mathbb{N}) \, \text{mul} \text{HasProd}(f\uparrow \mathbb{Z}_{<0})$$$
Lean4
@[to_additive HasSum.of_nat_of_neg_add_one]
theorem of_nat_of_neg_add_one {f : ℤ → M} (hf₁ : HasProd (fun n : ℕ ↦ f n) m)
(hf₂ : HasProd (fun n : ℕ ↦ f (-(n + 1))) m') : HasProd f (m * m') :=
by
have hi₂ : Injective Int.negSucc := @Int.negSucc.inj
have : IsCompl (Set.range ((↑) : ℕ → ℤ)) (Set.range Int.negSucc) :=
by
constructor
· rw [disjoint_iff_inf_le]
rintro _ ⟨⟨i, rfl⟩, ⟨j, ⟨⟩⟩⟩
· rw [codisjoint_iff_le_sup]
rintro (i | j) <;> simp
exact (Nat.cast_injective.hasProd_range_iff.mpr hf₁).mul_isCompl this (hi₂.hasProd_range_iff.mpr hf₂)
