English
For a sequence f: ℕ → G and a fixed k ∈ ℕ, HasProd of the shifted sequence (n ↦ f(n+k)) with a modified target g / ∏_{i∈range k} f(i) is equivalent to HasProd of the original sequence with target g.
Русский
Для последовательности f: ℕ → G и фиксированного k ∈ ℕ, HasProd под последовательностью сдвига (n ↦ f(n+k)) при целевом значении g/∏_{i<k} f(i) эквивалентна HasProd исходной последовательности с целевым значением g.
LaTeX
$$$$\\operatorname{HasProd}\\big(n\\mapsto f(n+k)\\big)\\Big(g/\\prod_{i∈\\mathrm{range}(k)} f(i)\\Big) \\iff \\operatorname{HasProd}\\big(n\\mapsto f(n)\\big)\\, g.$$$$
Lean4
@[to_additive]
theorem hasProd_nat_add_iff' {f : ℕ → G} (k : ℕ) : HasProd (fun n ↦ f (n + k)) (g / ∏ i ∈ range k, f i) ↔ HasProd f g :=
by simp [hasProd_nat_add_iff]
