eq_prod_range_div' — Mathlib

English

Let f: ℕ → G. Then f(n) = ∏_{i=0}^{n} [if i = 0 then f(0) else f(i)/f(i-1)].

Русский

Пусть f: ℕ → G. Тогда f(n) = ∏_{i=0}^{n} [если i = 0, то f(0), иначе f(i)/f(i-1)].

LaTeX

$$$$ f(n) = \\prod_{i=0}^{n} \\Big(\\text{if } i=0 \\text{ then } f(0) \\text{ else } \\frac{f(i)}{f(i-1)}\\Big) $$$$

Lean4

@[to_additive]
theorem eq_prod_range_div' (f : ℕ → G) (n : ℕ) : f n = ∏ i ∈ range (n + 1), if i = 0 then f 0 else f i / f (i - 1) :=
  by
  conv_lhs => rw [Finset.eq_prod_range_div f]
  simp [Finset.prod_range_succ', mul_comm]

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