English
For a group-valued sequence f: ℕ → G with IsTopologicalGroup structure in G, HasProd (fun n → f(n+k)) g is equivalent to HasProd f (g ∏_{i=0}^{k-1} f(i)) for any k, i.e., shifting indices corresponds to multiplying the target by the first k factors.
Русский
Для последовательности f: ℕ → G в группе с топологией HasProd (f(n+k)) g эквивалентно HasProd f (g ∏_{i=0}^{k-1} f(i)).
LaTeX
$$$\text{HasProd}(\lambda n. f(n+k))\, g \quad\text{iff}\quad \text{HasProd}(f)\left(g \cdot \prod_{i=0}^{k-1} f(i)\right).$$$
Lean4
@[to_additive]
theorem hasProd_nat_add_iff {f : ℕ → G} (k : ℕ) : HasProd (fun n ↦ f (n + k)) g ↔ HasProd f (g * ∏ i ∈ range k, f i) :=
by
refine Iff.trans ?_ (range k).hasProd_compl_iff
rw [← (notMemRangeEquiv k).symm.hasProd_iff, Function.comp_def, coe_notMemRangeEquiv_symm]
