English
If HasProd of nonnegative indices equals g and HasProd of negative indices equals g', then the bilateral product equals g g' / f(0).
Русский
Если произведение по неотрицательным индексам равно g, а по отрицательным — g', то двустороннее произведение равно g g' / f(0).
LaTeX
$$$\\displaystyle \\text{HasProd}\\ f\\ (g \\cdot g' / f(0)) \\leftarrow \\text{HasProd}((n\\mapsto f(n)), g) \\land \\text{HasProd}((n\\mapsto f(-n)), g')$$$
Lean4
@[to_additive]
theorem of_nat_of_neg {f : ℤ → G} (hf₁ : HasProd (fun n : ℕ ↦ f n) g) (hf₂ : HasProd (fun n : ℕ ↦ f (-n)) g') :
HasProd f (g * g' / f 0) :=
by
refine mul_div_assoc' g .. ▸ hf₁.of_nat_of_neg_add_one (m' := g' / f 0) ?_
rwa [← hasProd_nat_add_iff' 1, prod_range_one, Nat.cast_zero, neg_zero] at hf₂
