English
For a function f: ℕ → G, if f is multipliable then the finite-prefix product times the shifted tail product equals the full product: ∏_{i=0}^{k-1} f(i) · ∏' i, f(i+k) = ∏' i, f(i).
Русский
Для функции f: ℕ → G, если f удовлетворяет условию Multipliable, то произведение первых k членов умноженное на хвостовое произведение даёт полное произведение: ∏_{i=0}^{k-1} f(i) · ∏' i, f(i+k) = ∏' i, f(i).
LaTeX
$$$\left(\prod_{i=0}^{k-1} f(i)\right) \cdot \prod_{i=0}^{\infty} f(i+k) = \prod_{i=0}^{\infty} f(i).$$$
Lean4
@[to_additive]
theorem multipliable_nat_add_iff {f : ℕ → G} (k : ℕ) : (Multipliable fun n ↦ f (n + k)) ↔ Multipliable f :=
Iff.symm <|
(Equiv.mulRight (∏ i ∈ range k, f i)).surjective.multipliable_iff_of_hasProd_iff (hasProd_nat_add_iff k).symm
