Theorems · Theorem · combinatorics

Quiver.Path.weight.eq_def

∀ {V : Type u_1} [inst : Quiver V] {R : Type u_2} [inst_1 : Monoid R] (w : {i j : V} → (i ⟶ j) → R) (x x_1 : V)
  (x_2 : Quiver.Path x x_1),
  Quiver.Path.weight w x_2 =
    match x, x_1, x_2 with
    | a, .(a), Quiver.Path.nil => 1
    | a, x, p.cons e => Quiver.Path.weight (fun {i j} => w) p * w e

Defined in

Mathlib.Combinatorics.Quiver.Path.Weight

Cited by

0 results in Mathlib

Foundations

Depth 24 from the axioms · uses propext, Quot.sound

Assumes

QuiverMonoid