prod_range_succ — Mathlib

English

Let f: N → M be a function into a monoid M. Then the product over {0,...,n} equals the product over {0,...,n-1} times f(n): ∏_{k=0}^{n} f(k) = (∏_{k=0}^{n-1} f(k)) · f(n).

Русский

Пусть f: ℕ → M; тогда произведение по диапазону 0 ≤ k ≤ n равно произведению по диапазону 0 ≤ k < n, умноженному на f(n).

LaTeX

$$$ \bigl(\mathrm{range} \ n.succ\bigr).map f).prod = ((\mathrm{range} n).map f).prod \cdot f\,n $$$

Lean4

@[to_additive]
theorem prod_range_succ (f : ℕ → M) (n : ℕ) : ((range n.succ).map f).prod = ((range n).map f).prod * f n := by
  rw [range_succ, map_append, map_singleton, prod_append, prod_cons, prod_nil, mul_one]

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