prod_range_div' — Mathlib

English

For any n and function f, the product over k from 0 to n-1 of f(k+1)/f(k) equals f(n)/f(0).

Русский

Для функции f:Nat→G, произведение по k от 0 до n-1 дроби f(k+1)/f(k) равно f(n)/f(0).

LaTeX

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

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 / f (k + 1)).prod = f 0 / f n := by
  induction n with
  | zero => exact (div_self' (f 0)).symm
  | succ n h => rw [range_succ, map_append, map_singleton, prod_append, prod_singleton, h, div_mul_div_cancel]

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