Theorems · Theorem · combinatorics

Quiver.cast_eq_of_cons_eq_cons

∀ {U : Type u_1} [inst : Quiver U] {u v v' w : U} {p : Quiver.Path u v} {p' : Quiver.Path u v'} {e : v ⟶ w}
  {e' : v' ⟶ w} (h : p.cons e = p'.cons e'), Quiver.Path.cast ⋯ ⋯ p = p'

Defined in

Mathlib.Combinatorics.Quiver.Cast

Cited by

0 results in Mathlib

Foundations

Depth 9 from the axioms · uses propext

Assumes

Quiver