Theorems · Theorem · combinatorics

Quiver.Path.reverse.eq_def

∀ {V : Type u_2} [inst : Quiver V] [inst_1 : Quiver.HasReverse V] {a : V} (x : V) (x_1 : Quiver.Path a x),
  x_1.reverse =
    match x, x_1 with
    | .(a), Quiver.Path.nil => Quiver.Path.nil
    | x, p.cons e => (Quiver.reverse e).toPath.comp p.reverse

Defined in

Mathlib.Combinatorics.Quiver.Symmetric

Cited by

0 results in Mathlib

Foundations

Depth 10 from the axioms · uses no axioms

Assumes

QuiverQuiver.HasReverse