Documentation

Mathlib.Algebra.BigOperators.Sym

Lemmas on Finset.sum and Finset.prod involving Finset.sym2 or Finset.sym. #

theorem Finset.sum_sym2_filter_not_isDiag {ι : Type u_1} {α : Type u_2} [LinearOrder ι] [AddCommMonoid α] (s : Finset ι) (p : Sym2 ια) :
i{is.sym2 | ¬i.IsDiag}, p i = i{is.offDiag | i.1 < i.2}, p s(i.1, i.2)
theorem Finset.sum_count_of_mem_sym {α : Type u_1} [DecidableEq α] {m : } {k : Sym α m} {s : Finset α} (hk : k s.sym m) :
is, Multiset.count i k = m