Theorems · Theorem · combinatorics

Quiver.Path.weightOfEPs_comp

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

Defined in

Mathlib.Combinatorics.Quiver.Path.Weight

Cited by

0 results in Mathlib

Foundations

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

Assumes

QuiverMonoid