Theorems · Theorem · combinatorics

Quiver.Path.toList_comp

∀ {V : Type u} [inst : Quiver V] {a b : V} (p : Quiver.Path a b) {c : V} (q : Quiver.Path b c),
  (p.comp q).toList = q.toList ++ p.toList

Quiver.Path.toList is a contravariant functor. The inversion comes from Quiver.Path and List having different preferred directions for adding elements.

Defined in

Mathlib.Combinatorics.Quiver.Path

Cited by

0 results in Mathlib

Foundations

Depth 10 from the axioms · uses propext

Assumes

Quiver