Theorems · Definition · combinatorics
Sym2.equivSym
(α : Type u_4) → Sym2 α ≃ Sym α 2
The symmetric square is equivalent to the second symmetric power.
- Defined in
- Mathlib.Data.Sym.Sym2
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 28 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Equivstatement · cited by 8,337
- Equiv.symmproof · cited by 3,681
- Sym2statement · cited by 737
- Equiv.transproof · cited by 337
- Symstatement · cited by 150
- Sym.symEquivSym'proof · cited by 1
- Sym2.sym2EquivSym'proof · cited by 0
Cited by2
Results whose statement or proof uses this declaration.
- Sym2.equivMultisetproof · cited by 0
- List.sym2_eq_sym_twostatement and proof · cited by 0