prod_range_succ_div_top — Mathlib

English

Let f: N → M with M a commutative group. Then for every n ∈ N, (∏_{i=0}^{n} f(i)) / f(n) = ∏_{i=0}^{n-1} f(i).

Русский

Пусть f: ℕ → M, где M — коммутативная группа. Тогда для любого натурального n выполнено: (∏_{i=0}^{n} f(i)) / f(n) = ∏_{i=0}^{n-1} f(i).

LaTeX

$$$$ \\left( \\prod_{i=0}^{n} f(i) \\right) / f(n) = \\prod_{i=0}^{n-1} f(i). $$$$

Lean4

@[to_additive]
theorem prod_range_succ_div_top : (∏ i ∈ range (n + 1), f i) / f n = ∏ i ∈ range n, f i :=
  div_eq_iff_eq_mul.mpr <| prod_range_succ f n

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