Mathlib Map

Theorems · Definition · combinatorics

Quiver.Path.weight

{V : Type u_1} →
  [inst : Quiver V] → {R : Type u_2} → [Monoid R] → ({i j : V} → (i ⟶ j) → R) → {i j : V} → Quiver.Path i j → R

The weight of a path is the product of the weights of its edges.

Defined in
Mathlib.Combinatorics.Quiver.Path.Weight
Cited by
8 results in Mathlib
Foundations
Depth 23 from the axioms · uses propext
Assumes
QuiverMonoid
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Quiver.Path.weightOfEPs · cited by 5Path.weightOfEPsQuiver.Path.weight_cons · cited by 4Path.weight_consQuiver.Path.weight_nil · cited by 4Path.weight_nilQuiver.Path.weight_comp · cited by 1Path.weight_compQuiver.Path.weight_nonneg · cited by 1Path.weight_nonnegQuiver.Path.weight_pos · cited by 1Path.weight_posQuiver.Path.weight.eq_def · cited by 0weight.eq_defQuiver.Path.weightOfEPs_comp · cited by 0Path.weightOfEPs_compQuiver.Path.weightOfEPs_cons · cited by 0Path.weightOfEPs_consQuiver.Hom · cited by 32603Quiver.HomMonoid · cited by 3887MonoidQuiver · cited by 405QuiverQuiver.Path · cited by 166Quiver.PathPath.weightCITED BYCITES

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Quiver.Homstatement and proof · cited by 32,603
  • Monoidstatement and proof · cited by 3,887
  • Quiverstatement and proof · cited by 405
  • Quiver.Pathstatement and proof · cited by 166

Cited by9

Results whose statement or proof uses this declaration.