Theorems · Theorem · combinatorics
Multiset.eq_replicate
∀ {α : Type u_1} {a : α} {n : ℕ} {s : Multiset α}, s = Multiset.replicate n a ↔ s.card = n ∧ ∀ b ∈ s, b = a- Defined in
- Mathlib.Data.Multiset.Replicate
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 20 from the axioms · uses propext, Quot.sound
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.
- Multisetstatement and proof · cited by 2,627
- Multiset.cardstatement and proof · cited by 375
- Multiset.replicatestatement and proof · cited by 88
- Multiset.card_replicateproof · cited by 12
- Multiset.eq_of_mem_replicateproof · cited by 10
- Multiset.eq_replicate_of_memproof · cited by 3
Cited by9
Results whose statement or proof uses this declaration.
- IsDiscreteValuationRing.associated_pow_irreducibleproof · cited by 4
- Sym.eq_replicateproof · cited by 1
- Sym.eq_replicate_iffproof · cited by 1
- Equiv.Perm.cycleType_prime_orderproof · cited by 1
- Equiv.Perm.cycleType_of_pow_prime_eq_oneproof · cited by 1
- Multiset.replicate_right_injectiveproof · cited by 1
- PNat.count_factorMultisetproof · cited by 0
- Multiset.extract_gcdproof · cited by 0