Theorems · Theorem · combinatorics
Multiset.toFinset_singleton
∀ {α : Type u_1} [inst : DecidableEq α] (a : α), {a}.toFinset = {a}- Defined in
- Mathlib.Data.Finset.Insert
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 75 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.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetstatement and proof · cited by 13,712
- Multisetstatement and proof · cited by 2,627
- Multiset.toFinsetstatement and proof · cited by 230
- Multiset.toFinset_zeroproof · cited by 8
- Multiset.cons_zeroproof · cited by 5
- Multiset.toFinset_consproof · cited by 2
Cited by9
Results whose statement or proof uses this declaration.
- Polynomial.natSepDegree_X_sub_Cproof · cited by 4
- Polynomial.natSepDegree_Xproof · cited by 1
- DFinsupp.sumZeroHom_singleproof · cited by 1
- Polynomial.rootSet_monomialproof · cited by 1
- Equiv.Perm.card_of_cycleType_singletonproof · cited by 1
- UniqueFactorizationMonoid.radical_of_primeproof · cited by 1
- Finsupp.toFinset_toMultisetproof · cited by 1
- Multiset.toFinset_eq_singleton_iffproof · cited by 0
- Polynomial.SplittingFieldAux.adjoin_rootSetproof · cited by 0