Theorems · Theorem · combinatorics
Multiset.coe_eq_coe
∀ {α : Type u_1} {l₁ l₂ : List α}, ↑l₁ = ↑l₂ ↔ l₁.Perm l₂- Defined in
- Mathlib.Data.Multiset.Defs
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 13 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.ofListstatement · cited by 290
- Quotient.eqproof · cited by 50
Cited by11
Results whose statement or proof uses this declaration.
- Multiset.eq_replicate_cardproof · cited by 7
- PrimeMultiset.factorMultiset_prodproof · cited by 7
- Multiset.coe_eq_zeroproof · cited by 6
- List.perm_of_nodup_nodup_toFinset_eqproof · cited by 3
- Multiset.toList_eq_singleton_iffproof · cited by 2
- Multiset.bind_powerset_lenproof · cited by 2
- Finset.sort_perm_toListproof · cited by 1
- Multiset.revzip_powersetAux_permproof · cited by 0
- List.Subset.dedup_append_leftproof · cited by 0
- FreeCommRing.of_injectiveproof · cited by 0
- Multiset.coe_eq_singletonproof · cited by 0