prod_range_mul_prod_Ico — Mathlib

English

Let f: ℕ→M and m≤n. The product over range m times the product over Ico m n equals the product over range n: ∏_{k∈range m} f(k) · ∏_{k∈Ico m n} f(k) = ∏_{k∈range n} f(k).

Русский

Пусть f: ℕ→M и m≤n. Произведение по range m и затем по Ico m n даёт произведение по range n.

LaTeX

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

Lean4

@[to_additive]
theorem prod_range_mul_prod_Ico (f : ℕ → M) {m n : ℕ} (h : m ≤ n) :
    ((∏ k ∈ range m, f k) * ∏ k ∈ Ico m n, f k) = ∏ k ∈ range n, f k :=
  Nat.Ico_zero_eq_range ▸ Nat.Ico_zero_eq_range ▸ prod_Ico_consecutive f m.zero_le h

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