Theorems · Theorem · combinatorics

Quiver.Path.length.eq_def

∀ {V : Type u} [inst : Quiver V] {a : V} (x : V) (x_1 : Quiver.Path a x),
  x_1.length =
    match x, x_1 with
    | .(a), Quiver.Path.nil => 0
    | x, p.cons a_1 => p.length + 1

Defined in

Mathlib.Combinatorics.Quiver.Path

Cited by

0 results in Mathlib

Foundations

Depth 10 from the axioms · uses no axioms

Assumes

Quiver