Theorems · Theorem · order theory

Finset.prod_prod_Ioi_mul_eq_prod_prod_off_diag

∀ {α : Type u_1} {M : Type u_2} [inst : CommMonoid M] [inst_1 : LinearOrder α] [inst_2 : Fintype α]
  [inst_3 : LocallyFiniteOrderTop α] [LocallyFiniteOrderBot α] (f : α → α → M),
  ∏ i, ∏ j > i, f j i * f i j = ∏ i, ∏ j ∈ {i}ᶜ, f j i

Defined in

Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommMonoidLinearOrderFintypeLocallyFiniteOrderTopLocallyFiniteOrderBot