Theorems · Definition · combinatorics
Sym.replicate
{α : Type u_1} → (n : ℕ) → α → Sym α nreplicate n a is the sym containing only a with multiplicity n.
- Defined in
- Mathlib.Data.Sym.Basic
- Cited by
- 15 results in Mathlib
- Foundations
- Depth 13 from the axioms · uses propext
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.
- Symstatement · cited by 150
- Multiset.replicateproof · cited by 88
- Multiset.card_replicateproof · cited by 12
Cited by16
Results whose statement or proof uses this declaration.
- Sym.fillproof · cited by 11
- Sym.mem_replicatestatement · cited by 3
- Sym.coe_fillstatement · cited by 3
- Sym.coe_replicatestatement · cited by 3
- Finset.replicate_mem_symstatement and proof · cited by 2
- Finset.Nonempty.symproof · cited by 1
- Sym.eq_replicatestatement · cited by 1
- Sym.eq_replicate_iffstatement · cited by 1
- Sym.replicate_right_injstatement · cited by 1
- Sym.val_replicatestatement and proof · cited by 1
- Sym.fill_filterNeproof · cited by 1
- Sym.filter_ne_fillproof · cited by 1