Theorems · Theorem · combinatorics

Quiver.Path.weight_comp

∀ {V : Type u_1} [inst : Quiver V] {R : Type u_2} [inst_1 : Monoid R] (w : {i j : V} → (i ⟶ j) → R) {a b c : V}
  (p : Quiver.Path a b) (q : Quiver.Path b c),
  Quiver.Path.weight (fun {i j} => w) (p.comp q) =
    Quiver.Path.weight (fun {i j} => w) p * Quiver.Path.weight (fun {i j} => w) q

Defined in

Mathlib.Combinatorics.Quiver.Path.Weight

Cited by

1 results in Mathlib

Foundations

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

Assumes

QuiverMonoid