Theorems · Inductive type · combinatorics

Quiver.Path

{V : Type u} → [Quiver V] → V → V → Type (max u v)

Path a b is the type of paths from a to b through the arrows of G.

Defined in

Mathlib.Combinatorics.Quiver.Path

Cited by

166 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 2 definitions · uses no axioms

Assumes

Quiver