Theorems · Theorem · combinatorics
Multiset.cons_bind
∀ {α : Type u_1} {β : Type v} (a : α) (s : Multiset α) (f : α → Multiset β), (a ::ₘ s).bind f = f a + s.bind f- Defined in
- Mathlib.Data.Multiset.Bind
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 57 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
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.mapproof · cited by 876
- Multiset.consstatement · cited by 313
- Multiset.map_consproof · cited by 93
- Multiset.bindstatement · cited by 59
- Multiset.joinproof · cited by 21
- Multiset.join_consproof · cited by 9
Cited by13
Results whose statement or proof uses this declaration.
- Multiset.bind_mapproof · cited by 5
- Multiset.bind_singletonproof · cited by 5
- Multiset.bind_assocproof · cited by 4
- Multiset.cons_productproof · cited by 4
- Multiset.bind_consproof · cited by 2
- Multiset.fold_bindproof · cited by 1
- Multiset.filterMap_eq_bindproof · cited by 1
- Polynomial.roots_list_prodproof · cited by 1
- Multiset.cons_sigmaproof · cited by 1
- Finset.disjiUnion_consproof · cited by 1
- Multiset.filter_eq_bindproof · cited by 1
- Multiset.bind_bindproof · cited by 0