prod_range_div_prod_range — Mathlib

English

If n ≤ m, the quotient of the two range-products equals the product over k with n ≤ k < m: ∏_{k∈range m} f(k) / ∏_{k∈range n} f(k) = ∏_{k∈range m with n≤k} f(k).

Русский

Если n ≤ m, частное произведений по диапазонам равно произведению по k с n ≤ k < m.

LaTeX

$$$$ \\displaystyle \\frac{\\prod_{k \\in \\mathrm{range}(m)} f(k)}{\\prod_{k \\in \\mathrm{range}(n)} f(k)} = \\prod_{k \\in \\mathrm{range}(m) \\;\\text{с} \\;n\\le k} f(k). $$$$

Lean4

@[to_additive]
theorem prod_range_div_prod_range {G : Type*} [CommGroup G] {f : ℕ → G} {n m : ℕ} (hnm : n ≤ m) :
    ((∏ k ∈ range m, f k) / ∏ k ∈ range n, f k) = ∏ k ∈ range m with n ≤ k, f k :=
  by
  rw [← prod_Ico_eq_div f hnm]
  congr
  apply Finset.ext
  simp only [mem_Ico, mem_filter, mem_range, *]
  tauto

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