prod_range_eq_mul_Ico — Mathlib

English

For any f and n, the product over Ico m n can be written as the product over range n divided by the product over range m, i.e. ∏_{k∈Ico m n} f(k) = (∏_{k∈range n} f(k)) / (∏_{k∈range m} f(k)).

Русский

Для любого f и n произведение по Ico m n можно записать как отношение произведений по range n и range m.

LaTeX

$$$$ \\displaystyle \\prod_{k \\in \\mathrm{Ico}(m,n)} f(k) = \\frac{\\prod_{k \\in \\mathrm{range}(n)} f(k)}{\\prod_{k \\in \\mathrm{range}(m)} f(k)}. $$$$

Lean4

@[to_additive]
theorem prod_range_eq_mul_Ico (f : ℕ → M) {n : ℕ} (hn : 0 < n) : ∏ x ∈ Finset.range n, f x = f 0 * ∏ x ∈ Ico 1 n, f x :=
  Finset.range_eq_Ico ▸ Finset.prod_eq_prod_Ico_succ_bot hn f

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