prod_range_div — Mathlib

English

Cancellation of a telescoping product over a range: the product of f(k)/f(k+1) from k=0 to n-1 equals f(0)/f(n).

Русский

Редукция телескопического произведения по диапазону: произведение f(k)/f(k+1) от k=0 до n-1 равно f(0)/f(n).

LaTeX

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

Lean4

/-- Cancellation of a telescoping product. -/
@[to_additive /-- Cancellation of a telescoping sum. -/
    ]
theorem prod_range_div (n : ℕ) (f : ℕ → G) : ((range n).map fun k ↦ f (k + 1) / f k).prod = f n / f 0 :=
  by
  have h : ((·⁻¹) ∘ fun k ↦ f (k + 1) / f k) = fun k ↦ f k / f (k + 1) := by ext; apply inv_div
  rw [← inv_inj, prod_inv, map_map, inv_div, h, prod_range_div']

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