Theorems · Definition · combinatorics
Sym2.IsDiag
{α : Type u_1} → Sym2 α → PropA predicate for testing whether an element of Sym2 α is on the diagonal.
- Defined in
- Mathlib.Data.Sym.Sym2
- Cited by
- 43 results in Mathlib
- Foundations
- Depth 14 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.
- DFunLike.coeproof · cited by 62,936
- Sym2statement · cited by 737
- Sym2.liftproof · cited by 6
Cited by46
Results whose statement or proof uses this declaration.
- Sym2.diagSetproof · cited by 41
- SimpleGraph.not_isDiag_of_mem_edgeSetstatement · cited by 4
- Sym2.mk_isDiag_iffstatement · cited by 4
- Sym2.diagElemstatement and proof · cited by 4
- Sym2.diagElemEquivstatement and proof · cited by 4
- Sym2.fromRel_irreflstatement and proof · cited by 2
- Sym2.card_subtype_not_diagstatement and proof · cited by 2
- Sym2.card_toFinset_of_not_isDiagstatement and proof · cited by 2
- QuadraticMap.map_sumstatement and proof · cited by 2
- QuadraticMap.toQuadraticMap_toBilinproof · cited by 1
- QuadraticMap.apply_linearCombinationstatement and proof · cited by 1
- SimpleGraph.edgeDisjointTriangles_iff_mem_sym2_subsingletonstatement and proof · cited by 1