prod_mul_tprod_nat_add — Mathlib

English

If the shifted tail product ∏' i, f(i+k) is defined for all k and f is multipliable, then the finite-prefix times the tail equals the full product for each k.

Русский

Если хвостовое произведение сдвига f(i+k) определено и f — мультиплируемое, тогда для каждого k выполняется равенство указано выше.

LaTeX

$$$\bigl(\prod_{i\in\mathrm{range}(k)} f(i)\bigr) \cdot \prod_{i\in\mathbb{N}} f(i+k) = \prod_{i\in\mathbb{N}} f(i).$$$

Lean4

@[to_additive]
protected theorem prod_mul_tprod_nat_add [T2Space G] {f : ℕ → G} (k : ℕ) (h : Multipliable f) :
    ((∏ i ∈ range k, f i) * ∏' i, f (i + k)) = ∏' i, f i :=
  Multipliable.prod_mul_tprod_nat_mul' <| (multipliable_nat_add_iff k).2 h

Похожие утверждения