Theorems · Theorem · combinatorics
Multiset.count_sub
∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s t : Multiset α),
Multiset.count a (s - t) = Multiset.count a s - Multiset.count a t- Defined in
- Mathlib.Data.Multiset.AddSub
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 25 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- DecidableEq
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
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
- Multiset.coe_countproof · cited by 23
- List.count_diffproof · cited by 1
Cited by12
Results whose statement or proof uses this declaration.
- Multiset.count_interproof · cited by 9
- Multiset.count_unionproof · cited by 6
- Multiset.add_sub_cancel_rightproof · cited by 2
- Multiset.sub_add_cancelproof · cited by 2
- Multiset.add_sub_assocproof · cited by 1
- Multiset.mem_subproof · cited by 1
- Multiset.mem_sub_of_nodupproof · cited by 1
- Multiset.sub_add_eq_sub_subproof · cited by 1
- Multiset.inter_add_sub_of_add_eq_addproof · cited by 1
- Multiset.sub_singletonproof · cited by 0
- Multiset.add_sub_cancelproof · cited by 0
- Multiset.sub_filter_eq_filter_notproof · cited by 0