Mathlib Map

Theorems · Definition · combinatorics

Sym.mk

{α : Type u_1} → {n : ℕ} → (m : Multiset α) → m.card = n → Sym α n

Construct an element of the nth symmetric power from a multiset of cardinality n.

Defined in
Mathlib.Data.Sym.Basic
Cited by
8 results in Mathlib
Foundations
Depth 13 from the axioms · uses propext
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Sym.forall · cited by 0Sym.forallSym.mem_mk · cited by 0Sym.mem_mkSym.attach_mk · cited by 0Sym.attach_mkSym.mk.congr_simp · cited by 0mk.congr_simpSym.erase_mk · cited by 0Sym.erase_mkSym.exists · cited by 0Sym.existsSym.map_mk · cited by 0Sym.map_mkSym.coe_mk · cited by 0Sym.coe_mkMultiset · cited by 2627MultisetMultiset.card · cited by 375Multiset.cardSym · cited by 150SymSym.mkCITED BYCITES

Cites3

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
  • Symstatement · cited by 150

Cited by8

Results whose statement or proof uses this declaration.