prod_range_succ — Mathlib

English

For any function f: ℕ → M and n ∈ ℕ, the product over range (n+1) equals f(n) times the product over range n with commutation: ∏ x ∈ range (n+1), f x = f n · ∏ x ∈ range n, f x.

Русский

Для любой функции f: ℕ → M имеем: произведение по диапазону (n+1) равно f(n) умножить на произведение по диапазону n: ∏ x ∈ range (n+1), f x = f n · ∏ x ∈ range n, f x.

LaTeX

$$$\displaystyle \prod x \in \mathrm{range}(n+1), f(x) = f(n) \cdot \prod x \in \mathrm{range}(n), f(x)$$$

Lean4

@[to_additive]
theorem prod_range_succ (f : ℕ → M) (n : ℕ) : (∏ x ∈ range (n + 1), f x) = (∏ x ∈ range n, f x) * f n := by
  simp only [mul_comm, prod_range_succ_comm]

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