prod_range_succ' — Mathlib

English

A recurrence version: for f: ℕ → M and n, the product over range (n+1) equals the product over range n of f(k+1) times f(0) via a recursive relation.

Русский

Рекуррентная версия: произведение по range (n+1) равно произведению по range n от f(k+1) умножить на f(0).

LaTeX

$$$\displaystyle \prod_{k \in \mathrm{range}(n+1)} f(k) = \left(\prod_{k \in \mathrm{range}(n)} f(k+1)\right) \cdot f(0)$$$

Lean4

@[to_additive]
theorem prod_range_succ' (f : ℕ → M) : ∀ n : ℕ, (∏ k ∈ range (n + 1), f k) = (∏ k ∈ range n, f (k + 1)) * f 0
  | 0 => prod_range_succ _ _
  | n + 1 => by rw [prod_range_succ _ n, mul_right_comm, ← prod_range_succ' _ n, prod_range_succ]

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