Theorems · Theorem · combinatorics
Multiset.count_pos
∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Multiset α}, 0 < Multiset.count a s ↔ a ∈ s- Defined in
- Mathlib.Data.Multiset.Count
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 19 from the axioms · uses propext, Quot.sound
- Assumes
- DecidableEq
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Multisetstatement and proof · cited by 2,627
- Multiset.countstatement · cited by 302
Cited by12
Results whose statement or proof uses this declaration.
- Multiset.count_eq_zero_of_notMemproof · cited by 27
- Polynomial.mem_roots'proof · cited by 8
- Multiset.count_ne_zeroproof · cited by 5
- Multiset.one_le_count_iff_memproof · cited by 2
- Polynomial.isIntegral_coeff_of_factorsproof · cited by 1
- Multiset.mem_subproof · cited by 1
- Multiset.mem_sub_of_nodupproof · cited by 1
- Multiset.IsDershowitzMannaLT.transproof · cited by 0
- Multiset.coe_memproof · cited by 0
- Polynomial.normalizedFactors_cyclotomic_cardproof · cited by 0
- Polynomial.card_roots_le_derivativeproof · cited by 0
- Multiset.mem_of_mem_toEnumFinsetproof · cited by 0