Theorems · Theorem · combinatorics

Quiver.Path.vertices_comp_get_length_eq

∀ {V : Type u_1} [inst : Quiver V] {a b c : V} (p₁ : Quiver.Path a c) (p₂ : Quiver.Path c b)
  (h : autoParam (p₁.length < (p₁.comp p₂).vertices.length) Quiver.Path.vertices_comp_get_length_eq._auto_1),
  (p₁.comp p₂).vertices.get ⟨p₁.length, h⟩ = c

Defined in: Mathlib.Combinatorics.Quiver.Path.Vertices
Cited by: 0 results in Mathlib
Foundations: Depth 51 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Quiver

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites9

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

Quiverstatement and proof · cited by 405
add_tsub_cancel_rightproof · cited by 172
Quiver.Pathstatement and proof · cited by 166
Quiver.Path.compstatement and proof · cited by 45
Quiver.Path.lengthstatement and proof · cited by 39
Quiver.Path.verticesstatement and proof · cited by 21
Quiver.Path.vertices_lengthproof · cited by 5
Quiver.Path.getElem_vertices_zeroproof · cited by 2
Quiver.Path.vertices_compproof · cited by 2

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.