prod_Ico_eq_mul_inv — Mathlib

English

Over Ico, the product equals the product over the full range times the inverse of the prefix product: ∏_{k∈Ico m n} f(k) = (∏_{k∈range n} f(k)) (∏_{k∈range m} f(k))^{-1}.

Русский

Произведение по Ico м,n равно произведению по range n умножить на обратное к произведению по range m.

LaTeX

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

Lean4

@[to_additive]
theorem prod_Ico_eq_mul_inv {δ : Type*} [CommGroup δ] (f : ℕ → δ) {m n : ℕ} (h : m ≤ n) :
    ∏ k ∈ Ico m n, f k = (∏ k ∈ range n, f k) * (∏ k ∈ range m, f k)⁻¹ :=
  eq_mul_inv_iff_mul_eq.2 <| by (rw [mul_comm]; exact prod_range_mul_prod_Ico f h)

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