prod_range_div' — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem prod_range_div' (f : ℕ → G) (n : ℕ) : (∏ i ∈ range n, f i / f (i + 1)) = f 0 / f n := by
  apply prod_range_induction <;> simp

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