prod_Ico_eq_div — Mathlib

English

Using division, the same identity as in 2763 holds with division: ∏_{k∈Ico m n} f(k) = (∏_{k∈range n} f(k)) / (∏_{k∈range m} f(k)).

Русский

Через деление имеем то же равенство, что и в предыдущем случае: ...

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_Ico_eq_div {δ : Type*} [CommGroup δ] (f : ℕ → δ) {m n : ℕ} (h : m ≤ n) :
    ∏ k ∈ Ico m n, f k = (∏ k ∈ range n, f k) / ∏ k ∈ range m, f k := by
  simpa only [div_eq_mul_inv] using prod_Ico_eq_mul_inv f h

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