prod_range_div — Mathlib

English

Let G be a commutative group and f: ℕ → G. Then ∏_{i=0}^{n-1} f(i+1)/f(i) = f(n)/f(0).

Русский

Пусть G — коммутативная группа и f: ℕ → G. Тогда ∏_{i=0}^{n-1} f(i+1)/f(i) = f(n)/f(0).

LaTeX

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

Lean4

/-- A telescoping product along `{0, ..., n - 1}` of a commutative-group-valued function reduces to
the ratio of the last and first factors. -/
@[to_additive /-- A telescoping sum along `{0, ..., n - 1}` of a function valued in a commutative
    additive group reduces to the difference of the last and first terms. -/
    ]
theorem prod_range_div (f : ℕ → G) (n : ℕ) : (∏ i ∈ range n, f (i + 1) / f i) = f n / f 0 := by
  apply prod_range_induction <;> simp

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