eq_prod_range_div — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem eq_prod_range_div (f : ℕ → G) (n : ℕ) : f n = f 0 * ∏ i ∈ range n, f (i + 1) / f i := by
  rw [prod_range_div, mul_div_cancel]

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