Theorems · Theorem · order theory

Finset.prod_eq_prod_range_sdiff

∀ {α : Type u_3} {β : Type u_4} [inst : DecidableEq α] [inst_1 : CommMonoid β] (s : ℕ → Finset α),
  Monotone s →
    ∀ (g : α → β) (n : ℕ), ∏ i ∈ s n, g i = (∏ i ∈ s 0, g i) * ∏ i ∈ Finset.range n, ∏ j ∈ s (i + 1) \ s i, g j

Given a sequence of finite sets s₀ ⊆ s₁ ⊆ s₂ ⋯, the product of gᵢ over i ∈ sₙ is equal to ∏_{i ∈ s₀} gᵢ * ∏_{j < n, i ∈ sⱼ₊₁ \ sⱼ} gᵢ.

Defined in

Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Cited by

0 results in Mathlib

Foundations

Depth 80 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEqCommMonoid