Theorems · Theorem · combinatorics
Multiset.card_singleton
∀ {α : Type u_1} (a : α), {a}.card = 1- Defined in
- Mathlib.Data.Multiset.ZeroCons
- Cited by
- 17 results in Mathlib
- Foundations
- Depth 14 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Multisetstatement · cited by 2,627
- Multiset.cardstatement · cited by 375
- Multiset.card_consproof · cited by 19
Cited by17
Results whose statement or proof uses this declaration.
- Finset.card_singletonproof · cited by 144
- Multiset.card_pairproof · cited by 6
- Finsupp.card_toMultisetproof · cited by 5
- Equiv.Perm.IsThreeCycle.isCycleproof · cited by 3
- Equiv.Perm.closure_cycleType_eq_two_two_eq_alternatingGroupproof · cited by 2
- Multiset.countP_mapproof · cited by 2
- Multiset.esymm_pair_twoproof · cited by 1
- Equiv.Perm.cycleType_eq_two_two_subset_alternatingGroupproof · cited by 1
- Multiset.map_eq_singletonproof · cited by 1
- ADEInequality.admissible_of_one_lt_sumInvproof · cited by 1
- Multiset.card_piproof · cited by 1
- alternatingGroup.mem_kleinFour_of_order_two_powproof · cited by 1