Theorems · Theorem · combinatorics

Finset.sum_sym2_filter_not_isDiag

∀ {ι : Type u_1} {M : Type u_2} [inst : LinearOrder ι] [inst_1 : AddCommMonoid M] (s : Finset ι) (p : Sym2 ι → M),
  ∑ i ∈ s.sym2 with ¬i.IsDiag, p i = ∑ i ∈ s.offDiag with i.1 < i.2, p s(i.1, i.2)

Defined in

Mathlib.Algebra.BigOperators.Sym

Cited by

1 results in Mathlib

Foundations

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

Assumes

LinearOrderAddCommMonoid