prod_range_add_div_prod_range — Mathlib

English

For f: ℕ → G, and natural numbers n,m, (∏_{k=0}^{n+m-1} f(k)) / (∏_{k=0}^{n-1} f(k)) = ∏_{k=0}^{m-1} f(n+k).

Русский

Для f: ℕ → G и натуральных n,m: (∏_{k=0}^{n+m-1} f(k)) / (∏_{k=0}^{n-1} f(k)) = ∏_{k=0}^{m-1} f(n+k).

LaTeX

$$$$ \\dfrac{\\prod_{k=0}^{n+m-1} f(k)}{\\prod_{k=0}^{n-1} f(k)} = \\prod_{k=0}^{m-1} f(n+k) $$$$

Lean4

@[to_additive]
theorem prod_range_add_div_prod_range (f : ℕ → G) (n m : ℕ) :
    (∏ k ∈ range (n + m), f k) / ∏ k ∈ range n, f k = ∏ k ∈ Finset.range m, f (n + k) :=
  div_eq_of_eq_mul' (prod_range_add f n m)

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