Sym

Statistics

Metric	Count
Definitions	0
Theorems `sum_count_of_mem_sym`, `sum_sym2_filter_not_isDiag`	2
Total	2

Name	Kind	Assumes	Proves	Validates	Depends On
`sum_count_of_mem_sym` 📖	mathematical	`Sym` `Finset` `instMembership` `sym`	`sum` `Nat.instAddCommMonoid` `Multiset.count` `Sym.toMultiset`	—	`Multiset.sum_count_eq_card` `Sym.card_coe`
`sum_sym2_filter_not_isDiag` 📖	mathematical	—	`sum` `Sym2` `filter` `Sym2.IsDiag` `Sym2.IsDiag.decidablePred` `LinearOrder.toDecidableEq` `sym2` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrder.toDecidableLT` `offDiag`	—	`offDiag_filter_lt_eq_filter_le` `sum_subtype_eq_sum_filter` `sum_equiv`

---