Mathlib Map

Theorems · Definition · combinatorics

Quiver.Symmetrify

Type u_1 → Type u_1

A type synonym for the symmetrized quiver (with an arrow both ways for each original arrow).

Defined in
Mathlib.Combinatorics.Quiver.Symmetric
Cited by
28 results in Mathlib
Foundations
Depth 0 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Quiver.Symmetrify.of · cited by 9Symmetrify.ofQuiver.FreeGroupoid.redStep · cited by 7FreeGroupoid.redStepQuiver.Symmetrify.lift · cited by 5Symmetrify.liftPrefunctor.symmetrify · cited by 5Prefunctor.symmetrifyIsFreeGroupoid.SpanningTree.homOfPath · cited by 4SpanningTree.homOfPathIsFreeGroupoid.SpanningTree.treeHom · cited by 4SpanningTree.treeHomQuiver.FreeGroupoid.lift_unique · cited by 3FreeGroupoid.lift_uniqueIsFreeGroupoid.SpanningTree.functorOfMonoidHom · cited by 3SpanningTree.functorOfMon…IsFreeGroupoid.SpanningTree.loopOfHom · cited by 3SpanningTree.loopOfHomIsFreeGroupoid.SpanningTree.treeHom_eq · cited by 2SpanningTree.treeHom_eqPrefunctor.symmetrify_map · cited by 2Prefunctor.symmetrify_mapQuiver.symmetrifyCostar · cited by 2Quiver.symmetrifyCostarPrefunctor.symmetrify_obj · cited by 2Prefunctor.symmetrify_objQuiver.symmetrifyStar · cited by 2Quiver.symmetrifyStarQuiver.wideSubquiverSymmetrify · cited by 2Quiver.wideSubquiverSymme…Quiver.SymmetrifyCITED BYCITES

Cites0

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Nothing in Mathlib beyond the foundations.

Cited by45

Results whose statement or proof uses this declaration.