Loogle!

Result

Found 167 declarations mentioning Quiver.Path.

• Quiver.Path 📋 Mathlib.Combinatorics.Quiver.Path
  {V : Type u} [Quiver V] (a : V) : V → Type (max u v)
• Quiver.Path.nil 📋 Mathlib.Combinatorics.Quiver.Path
  {V : Type u} [Quiver V] {a : V} : Quiver.Path a a
• Quiver.Path.instInhabited 📋 Mathlib.Combinatorics.Quiver.Path
  {V : Type u} [Quiver V] {a : V} : Inhabited (Quiver.Path a a)
• Quiver.Path.length 📋 Mathlib.Combinatorics.Quiver.Path
  {V : Type u} [Quiver V] {a b : V} : Quiver.Path a b → ℕ
• Quiver.Path.toList 📋 Mathlib.Combinatorics.Quiver.Path
  {V : Type u} [Quiver V] {a b : V} : Quiver.Path a b → List V
• Quiver.Hom.toPath 📋 Mathlib.Combinatorics.Quiver.Path
  {V : Type u_1} [Quiver V] {a b : V} (e : a ⟶ b) : Quiver.Path a b
• Quiver.Path.reachable 📋 Mathlib.Combinatorics.Quiver.Path
  {V : Type u} [Quiver V] {a b : V} (p : Quiver.Path a b) : Quiver.Reachable a b
• Quiver.Reachable.elim 📋 Mathlib.Combinatorics.Quiver.Path
  {V : Type u} [Quiver V] {a b : V} {p : Prop} (h : Quiver.Reachable a b) (hp : ∀ (a : Quiver.Path a b), p) : p
• Quiver.Path.comp 📋 Mathlib.Combinatorics.Quiver.Path
  {V : Type u} [Quiver V] {a b c : V} : Quiver.Path a b → Quiver.Path b c → Quiver.Path a c
• Quiver.Path.cons 📋 Mathlib.Combinatorics.Quiver.Path
  {V : Type u} [Quiver V] {a b c : V} : Quiver.Path a b → (b ⟶ c) → Quiver.Path a c
• Quiver.Path.instDecidableEq 📋 Mathlib.Combinatorics.Quiver.Path
  {V : Type u_1} [Quiver V] [DecidableEq V] [(v w : V) → DecidableEq (v ⟶ w)] (v w : V) : DecidableEq (Quiver.Path v w)
• Quiver.Path.isChain_toList_nonempty 📋 Mathlib.Combinatorics.Quiver.Path
  {V : Type u} [Quiver V] {a b : V} (p : Quiver.Path a b) : List.IsChain (fun x y => Nonempty (y ⟶ x)) p.toList
• Quiver.Path.toList_injective 📋 Mathlib.Combinatorics.Quiver.Path
  {V : Type u} [Quiver V] [∀ (a b : V), Subsingleton (a ⟶ b)] (a b : V) : Function.Injective Quiver.Path.toList
• Quiver.Path.eq_of_length_zero 📋 Mathlib.Combinatorics.Quiver.Path
  {V : Type u} [Quiver V] {a b : V} (p : Quiver.Path a b) (hzero : p.length = 0) : a = b
• Quiver.Path.comp_nil 📋 Mathlib.Combinatorics.Quiver.Path
  {V : Type u} [Quiver V] {a b : V} (p : Quiver.Path a b) : p.comp Quiver.Path.nil = p
• Quiver.Path.nil_comp 📋 Mathlib.Combinatorics.Quiver.Path
  {V : Type u} [Quiver V] {a b : V} (p : Quiver.Path a b) : Quiver.Path.nil.comp p = p
• Quiver.Path.comp_injective_right 📋 Mathlib.Combinatorics.Quiver.Path
  {V : Type u} [Quiver V] {a b c : V} (p : Quiver.Path a b) : Function.Injective p.comp
• Quiver.Path.isChain_cons_toList_nonempty 📋 Mathlib.Combinatorics.Quiver.Path
  {V : Type u} [Quiver V] {a b : V} (p : Quiver.Path a b) : List.IsChain (fun x y => Nonempty (y ⟶ x)) (b :: p.toList)
• Quiver.Path.cons_ne_nil 📋 Mathlib.Combinatorics.Quiver.Path
  {V : Type u} [Quiver V] {a b : V} (p : Quiver.Path a b) (e : b ⟶ a) : p.cons e ≠ Quiver.Path.nil
• Quiver.Path.eq_nil_of_length_zero 📋 Mathlib.Combinatorics.Quiver.Path
  {V : Type u} [Quiver V] {a : V} (p : Quiver.Path a a) (hzero : p.length = 0) : p = Quiver.Path.nil
• Quiver.Path.nil_ne_cons 📋 Mathlib.Combinatorics.Quiver.Path
  {V : Type u} [Quiver V] {a b : V} (p : Quiver.Path a b) (e : b ⟶ a) : Quiver.Path.nil ≠ p.cons e
• Prefunctor.mapPath 📋 Mathlib.Combinatorics.Quiver.Path
  {V : Type u₁} [Quiver V] {W : Type u₂} [Quiver W] (F : V ⥤q W) {a b : V} : Quiver.Path a b → Quiver.Path (F.obj a) (F.obj b)
• Quiver.Path.comp_injective_left 📋 Mathlib.Combinatorics.Quiver.Path
  {V : Type u} [Quiver V] {a b c : V} (q : Quiver.Path b c) : Function.Injective fun p => p.comp q
• Quiver.Path.comp_toPath_eq_cons 📋 Mathlib.Combinatorics.Quiver.Path
  {V : Type u_1} [Quiver V] {a b c : V} (p : Quiver.Path a b) (e : b ⟶ c) : p.comp e.toPath = p.cons e
• Prefunctor.mapPath_id 📋 Mathlib.Combinatorics.Quiver.Path
  {V : Type u₁} [Quiver V] {a b : V} (p : Quiver.Path a b) : (𝟭q V).mapPath p = p
• Quiver.Path.toList_inj 📋 Mathlib.Combinatorics.Quiver.Path
  {V : Type u} [Quiver V] {a b : V} [∀ (a b : V), Subsingleton (a ⟶ b)] {p q : Quiver.Path a b} : p.toList = q.toList ↔ p = q
• Quiver.Path.length_cons 📋 Mathlib.Combinatorics.Quiver.Path
  {V : Type u} [Quiver V] (a b c : V) (p : Quiver.Path a b) (e : b ⟶ c) : (p.cons e).length = p.length + 1
• Quiver.Path.length_comp 📋 Mathlib.Combinatorics.Quiver.Path
  {V : Type u} [Quiver V] {a b : V} (p : Quiver.Path a b) {c : V} (q : Quiver.Path b c) : (p.comp q).length = p.length + q.length
• Prefunctor.mapPath_nil 📋 Mathlib.Combinatorics.Quiver.Path
  {V : Type u₁} [Quiver V] {W : Type u₂} [Quiver W] (F : V ⥤q W) (a : V) : F.mapPath Quiver.Path.nil = Quiver.Path.nil
• Quiver.Path.comp_inj_left 📋 Mathlib.Combinatorics.Quiver.Path
  {V : Type u} [Quiver V] {a b c : V} {p₁ p₂ : Quiver.Path a b} {q : Quiver.Path b c} : p₁.comp q = p₂.comp q ↔ p₁ = p₂
• Quiver.Path.comp_inj_right 📋 Mathlib.Combinatorics.Quiver.Path
  {V : Type u} [Quiver V] {a b c : V} {p : Quiver.Path a b} {q₁ q₂ : Quiver.Path b c} : p.comp q₁ = p.comp q₂ ↔ q₁ = q₂
• Quiver.Path.obj_eq_of_cons_eq_cons 📋 Mathlib.Combinatorics.Quiver.Path
  {V : Type u} [Quiver V] {a b c d : V} {p : Quiver.Path a b} {p' : Quiver.Path a c} {e : b ⟶ d} {e' : c ⟶ d} (h : p.cons e = p'.cons e') : b = c
• Quiver.Path.toList_comp 📋 Mathlib.Combinatorics.Quiver.Path
  {V : Type u} [Quiver V] {a b : V} (p : Quiver.Path a b) {c : V} (q : Quiver.Path b c) : (p.comp q).toList = q.toList ++ p.toList
• Quiver.Path.comp_assoc 📋 Mathlib.Combinatorics.Quiver.Path
  {V : Type u} [Quiver V] {a b c d : V} (p : Quiver.Path a b) (q : Quiver.Path b c) (r : Quiver.Path c d) : (p.comp q).comp r = p.comp (q.comp r)
• Quiver.Path.comp_cons 📋 Mathlib.Combinatorics.Quiver.Path
  {V : Type u} [Quiver V] {a b c d : V} (p : Quiver.Path a b) (q : Quiver.Path b c) (e : c ⟶ d) : p.comp (q.cons e) = (p.comp q).cons e
• Quiver.Path.heq_of_cons_eq_cons 📋 Mathlib.Combinatorics.Quiver.Path
  {V : Type u} [Quiver V] {a b c d : V} {p : Quiver.Path a b} {p' : Quiver.Path a c} {e : b ⟶ d} {e' : c ⟶ d} (h : p.cons e = p'.cons e') : p ≍ p'
• Quiver.Path.hom_heq_of_cons_eq_cons 📋 Mathlib.Combinatorics.Quiver.Path
  {V : Type u} [Quiver V] {a b c d : V} {p : Quiver.Path a b} {p' : Quiver.Path a c} {e : b ⟶ d} {e' : c ⟶ d} (h : p.cons e = p'.cons e') : e ≍ e'
• Quiver.Path.length_ne_zero_iff_eq_cons 📋 Mathlib.Combinatorics.Quiver.Path
  {V : Type u_1} [Quiver V] {a b : V} (p : Quiver.Path a b) : p.length ≠ 0 ↔ ∃ c p' e, p = p'.cons e
• Prefunctor.mapPath_toPath 📋 Mathlib.Combinatorics.Quiver.Path
  {V : Type u₁} [Quiver V] {W : Type u₂} [Quiver W] (F : V ⥤q W) {a b : V} (f : a ⟶ b) : F.mapPath f.toPath = (F.map f).toPath
• Quiver.Path.comp_inj 📋 Mathlib.Combinatorics.Quiver.Path
  {V : Type u} [Quiver V] {a b c : V} {p₁ p₂ : Quiver.Path a b} {q₁ q₂ : Quiver.Path b c} (hq : q₁.length = q₂.length) : p₁.comp q₁ = p₂.comp q₂ ↔ p₁ = p₂ ∧ q₁ = q₂
• Quiver.Path.comp_inj' 📋 Mathlib.Combinatorics.Quiver.Path
  {V : Type u} [Quiver V] {a b c : V} {p₁ p₂ : Quiver.Path a b} {q₁ q₂ : Quiver.Path b c} (h : p₁.length = p₂.length) : p₁.comp q₁ = p₂.comp q₂ ↔ p₁ = p₂ ∧ q₁ = q₂
• Quiver.Path.eq_toPath_comp_of_length_eq_succ 📋 Mathlib.Combinatorics.Quiver.Path
  {V : Type u} [Quiver V] {a b : V} (p : Quiver.Path a b) {n : ℕ} (hp : p.length = n + 1) : ∃ c f q, ∃ (_ : q.length = n), p = f.toPath.comp q
• Quiver.Path.length_ne_zero_iff_eq_comp 📋 Mathlib.Combinatorics.Quiver.Path
  {V : Type u_1} [Quiver V] {a b : V} (p : Quiver.Path a b) : p.length ≠ 0 ↔ ∃ c e p', p = e.toPath.comp p' ∧ p.length = p'.length + 1
• Prefunctor.mapPath_comp 📋 Mathlib.Combinatorics.Quiver.Path
  {V : Type u₁} [Quiver V] {W : Type u₂} [Quiver W] (F : V ⥤q W) {a b : V} (p : Quiver.Path a b) {c : V} (q : Quiver.Path b c) : F.mapPath (p.comp q) = (F.mapPath p).comp (F.mapPath q)
• Prefunctor.mapPath_cons 📋 Mathlib.Combinatorics.Quiver.Path
  {V : Type u₁} [Quiver V] {W : Type u₂} [Quiver W] (F : V ⥤q W) {a b c : V} (p : Quiver.Path a b) (e : b ⟶ c) : F.mapPath (p.cons e) = (F.mapPath p).cons (F.map e)
• Prefunctor.mapPath_comp_apply 📋 Mathlib.Combinatorics.Quiver.Path
  {V : Type u₁} [Quiver V] {W : Type u₂} [Quiver W] (F : V ⥤q W) {U : Type u₃} [Quiver U] (G : W ⥤q U) {a b : V} (p : Quiver.Path a b) : (F ⋙q G).mapPath p = G.mapPath (F.mapPath p)
• Quiver.Path.reverse 📋 Mathlib.Combinatorics.Quiver.Symmetric
  {V : Type u_2} [Quiver V] [Quiver.HasReverse V] {a b : V} : Quiver.Path a b → Quiver.Path b a
• Quiver.Path.reverse_reverse 📋 Mathlib.Combinatorics.Quiver.Symmetric
  {V : Type u_2} [Quiver V] [h : Quiver.HasInvolutiveReverse V] {a b : V} (p : Quiver.Path a b) : p.reverse.reverse = p
• Quiver.Path.reverse_toPath 📋 Mathlib.Combinatorics.Quiver.Symmetric
  {V : Type u_2} [Quiver V] [Quiver.HasReverse V] {a b : V} (f : a ⟶ b) : f.toPath.reverse = (Quiver.reverse f).toPath
• Quiver.Path.reverse_comp 📋 Mathlib.Combinatorics.Quiver.Symmetric
  {V : Type u_2} [Quiver V] [Quiver.HasReverse V] {a b c : V} (p : Quiver.Path a b) (q : Quiver.Path b c) : (p.comp q).reverse = q.reverse.comp p.reverse
• CategoryTheory.composePath 📋 Mathlib.CategoryTheory.PathCategory.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} : Quiver.Path X Y → (X ⟶ Y)
• CategoryTheory.Paths.of_map 📋 Mathlib.CategoryTheory.PathCategory.Basic
  (V : Type u₁) [Quiver V] {X✝ Y✝ : V} (f : X✝ ⟶ Y✝) : (CategoryTheory.Paths.of V).map f = f.toPath
• CategoryTheory.composePath_cons 📋 Mathlib.CategoryTheory.PathCategory.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (p : Quiver.Path X Y) (e : Y ⟶ Z) : CategoryTheory.composePath (p.cons e) = CategoryTheory.CategoryStruct.comp (CategoryTheory.composePath p) e
• CategoryTheory.composePath_comp 📋 Mathlib.CategoryTheory.PathCategory.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (f : Quiver.Path X Y) (g : Quiver.Path Y Z) : CategoryTheory.composePath (f.comp g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.composePath f) (CategoryTheory.composePath g)
• CategoryTheory.Prefunctor.mapPath_comp' 📋 Mathlib.CategoryTheory.PathCategory.Basic
  (V : Type u₁) [Quiver V] (W : Type u₂) [Quiver W] (F : V ⥤q W) {X Y Z : CategoryTheory.Paths V} (f : X ⟶ Y) (g : Y ⟶ Z) : F.mapPath (CategoryTheory.CategoryStruct.comp f g) = (F.mapPath f).comp (F.mapPath g)
• CategoryTheory.Paths.lift_cons 📋 Mathlib.CategoryTheory.PathCategory.Basic
  {V : Type u₁} [Quiver V] {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (φ : V ⥤q C) {X Y Z : V} (p : Quiver.Path X Y) (f : Y ⟶ Z) : (CategoryTheory.Paths.lift φ).map (p.cons f) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Paths.lift φ).map p) (φ.map f)
• CategoryTheory.MorphismProperty.composePath_mem 📋 Mathlib.CategoryTheory.PathCategory.MorphismProperty
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (W : CategoryTheory.MorphismProperty C) [W.IsMultiplicative] {X Y : C} {p : Quiver.Path X Y} (hp : W.paths p) : W (CategoryTheory.composePath p)
• CategoryTheory.MorphismProperty.composePath_mem_of_id_mem 📋 Mathlib.CategoryTheory.PathCategory.MorphismProperty
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (W : CategoryTheory.MorphismProperty C) [W.IsStableUnderComposition] {X Y : C} {p : Quiver.Path X Y} (hp : W.paths p) (h : W (CategoryTheory.CategoryStruct.id X)) : W (CategoryTheory.composePath p)
• CategoryTheory.MorphismProperty.composePath_mem_of_length_pos 📋 Mathlib.CategoryTheory.PathCategory.MorphismProperty
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (W : CategoryTheory.MorphismProperty C) [W.IsStableUnderComposition] {X Y : C} {p : Quiver.Path X Y} (hp : W.paths p) (h : 0 < p.length) : W (CategoryTheory.composePath p)
• CategoryTheory.MorphismProperty.cons_mem_paths 📋 Mathlib.CategoryTheory.PathCategory.MorphismProperty
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y Z : C} {p : Quiver.Path X Y} {f : Y ⟶ Z} (hp : W.paths p) (hf : W f) : W.paths (p.cons f)
• CategoryTheory.MorphismProperty.cons_mem_paths_iff 📋 Mathlib.CategoryTheory.PathCategory.MorphismProperty
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y Z : C} {p : Quiver.Path X Y} {f : Y ⟶ Z} : W.paths (p.cons f) ↔ W.paths p ∧ W f
• CategoryTheory.MorphismProperty.comp_mem_paths_iff 📋 Mathlib.CategoryTheory.PathCategory.MorphismProperty
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y Z : C} {p : Quiver.Path X Y} {q : Quiver.Path Y Z} : W.paths (p.comp q) ↔ W.paths p ∧ W.paths q
• CategoryTheory.Cat.freeMap_map 📋 Mathlib.CategoryTheory.Category.Quiv
  {V : Type u_1} {W : Type u_2} [Quiver V] [Quiver W] (F : V ⥤q W) {X✝ Y✝ : CategoryTheory.Paths V} (a✝ : Quiver.Path X✝ Y✝) : (CategoryTheory.Cat.freeMap F).map a✝ = F.mapPath a✝
• Quiver.Path.cast 📋 Mathlib.Combinatorics.Quiver.Cast
  {U : Type u_1} [Quiver U] {u v u' v' : U} (hu : u = u') (hv : v = v') (p : Quiver.Path u v) : Quiver.Path u' v'
• Quiver.Path.cast_rfl_rfl 📋 Mathlib.Combinatorics.Quiver.Cast
  {U : Type u_1} [Quiver U] {u v : U} (p : Quiver.Path u v) : Quiver.Path.cast ⋯ ⋯ p = p
• Quiver.Path.cast_nil 📋 Mathlib.Combinatorics.Quiver.Cast
  {U : Type u_1} [Quiver U] {u u' : U} (hu : u = u') : Quiver.Path.cast hu hu Quiver.Path.nil = Quiver.Path.nil
• Quiver.Path.cast_heq 📋 Mathlib.Combinatorics.Quiver.Cast
  {U : Type u_1} [Quiver U] {u v u' v' : U} (hu : u = u') (hv : v = v') (p : Quiver.Path u v) : Quiver.Path.cast hu hv p ≍ p
• Quiver.eq_nil_of_length_zero 📋 Mathlib.Combinatorics.Quiver.Cast
  {U : Type u_1} [Quiver U] {u v : U} (p : Quiver.Path u v) (hzero : p.length = 0) : Quiver.Path.cast ⋯ ⋯ p = Quiver.Path.nil
• Quiver.Path.cast_eq_iff_heq 📋 Mathlib.Combinatorics.Quiver.Cast
  {U : Type u_1} [Quiver U] {u v u' v' : U} (hu : u = u') (hv : v = v') (p : Quiver.Path u v) (p' : Quiver.Path u' v') : Quiver.Path.cast hu hv p = p' ↔ p ≍ p'
• Quiver.Path.eq_cast_iff_heq 📋 Mathlib.Combinatorics.Quiver.Cast
  {U : Type u_1} [Quiver U] {u v u' v' : U} (hu : u = u') (hv : v = v') (p : Quiver.Path u v) (p' : Quiver.Path u' v') : p' = Quiver.Path.cast hu hv p ↔ p' ≍ p
• Quiver.Path.cast_eq_cast 📋 Mathlib.Combinatorics.Quiver.Cast
  {U : Type u_1} [Quiver U] {u v u' v' : U} (hu : u = u') (hv : v = v') (p : Quiver.Path u v) : Quiver.Path.cast hu hv p = cast ⋯ p
• Quiver.Path.cast_cast 📋 Mathlib.Combinatorics.Quiver.Cast
  {U : Type u_1} [Quiver U] {u v u' v' u'' v'' : U} (p : Quiver.Path u v) (hu : u = u') (hv : v = v') (hu' : u' = u'') (hv' : v' = v'') : Quiver.Path.cast hu' hv' (Quiver.Path.cast hu hv p) = Quiver.Path.cast ⋯ ⋯ p
• Quiver.cast_eq_of_cons_eq_cons 📋 Mathlib.Combinatorics.Quiver.Cast
  {U : Type u_1} [Quiver U] {u v v' w : U} {p : Quiver.Path u v} {p' : Quiver.Path u v'} {e : v ⟶ w} {e' : v' ⟶ w} (h : p.cons e = p'.cons e') : Quiver.Path.cast ⋯ ⋯ p = p'
• Quiver.hom_cast_eq_of_cons_eq_cons 📋 Mathlib.Combinatorics.Quiver.Cast
  {U : Type u_1} [Quiver U] {u v v' w : U} {p : Quiver.Path u v} {p' : Quiver.Path u v'} {e : v ⟶ w} {e' : v' ⟶ w} (h : p.cons e = p'.cons e') : Quiver.Hom.cast ⋯ ⋯ e = e'
• Quiver.Path.cast_cons 📋 Mathlib.Combinatorics.Quiver.Cast
  {U : Type u_1} [Quiver U] {u v w u' w' : U} (p : Quiver.Path u v) (e : v ⟶ w) (hu : u = u') (hw : w = w') : Quiver.Path.cast hu hw (p.cons e) = (Quiver.Path.cast hu ⋯ p).cons (Quiver.Hom.cast ⋯ hw e)
• Quiver.SingleObj.listToPath 📋 Mathlib.Combinatorics.Quiver.SingleObj
  {α : Type u_1} : List α → Quiver.Path (Quiver.SingleObj.star α) (Quiver.SingleObj.star α)
• Quiver.SingleObj.pathEquivList 📋 Mathlib.Combinatorics.Quiver.SingleObj
  {α : Type u_1} : Quiver.Path (Quiver.SingleObj.star α) (Quiver.SingleObj.star α) ≃ List α
• Quiver.SingleObj.pathToList 📋 Mathlib.Combinatorics.Quiver.SingleObj
  {α : Type u_1} {x : Quiver.SingleObj α} : Quiver.Path (Quiver.SingleObj.star α) x → List α
• Quiver.SingleObj.listToPath_pathToList 📋 Mathlib.Combinatorics.Quiver.SingleObj
  {α : Type u_1} {x : Quiver.SingleObj α} (p : Quiver.Path (Quiver.SingleObj.star α) x) : Quiver.SingleObj.listToPath (Quiver.SingleObj.pathToList p) = Quiver.Path.cast ⋯ ⋯ p
• Quiver.SingleObj.pathEquivList_nil 📋 Mathlib.Combinatorics.Quiver.SingleObj
  {α : Type u_1} : Quiver.SingleObj.pathEquivList Quiver.Path.nil = []
• Quiver.SingleObj.pathEquivList_symm_nil 📋 Mathlib.Combinatorics.Quiver.SingleObj
  {α : Type u_1} : Quiver.SingleObj.pathEquivList.symm [] = Quiver.Path.nil
• Quiver.SingleObj.pathEquivList_cons 📋 Mathlib.Combinatorics.Quiver.SingleObj
  {α : Type u_1} (p : Quiver.Path (Quiver.SingleObj.star α) (Quiver.SingleObj.star α)) (a : Quiver.SingleObj.star α ⟶ Quiver.SingleObj.star α) : Quiver.SingleObj.pathEquivList (p.cons a) = a :: Quiver.SingleObj.pathToList p
• Quiver.SingleObj.pathEquivList_symm_cons 📋 Mathlib.Combinatorics.Quiver.SingleObj
  {α : Type u_1} (l : List α) (a : α) : Quiver.SingleObj.pathEquivList.symm (a :: l) = (Quiver.SingleObj.pathEquivList.symm l).cons a
• CategoryTheory.FreeBicategory.inclusionPathAux 📋 Mathlib.CategoryTheory.Bicategory.Coherence
  {B : Type u} [Quiver B] {a b : B} : Quiver.Path a b → CategoryTheory.FreeBicategory.Hom a b
• CategoryTheory.FreeBicategory.normalizeAux 📋 Mathlib.CategoryTheory.Bicategory.Coherence
  {B : Type u} [Quiver B] {a b c : B} : Quiver.Path a b → CategoryTheory.FreeBicategory.Hom b c → Quiver.Path a c
• CategoryTheory.FreeBicategory.inclusionPath 📋 Mathlib.CategoryTheory.Bicategory.Coherence
  {B : Type u} [Quiver B] (a b : B) : CategoryTheory.Functor (CategoryTheory.Discrete (Quiver.Path a b)) (CategoryTheory.FreeBicategory.Hom a b)
• CategoryTheory.FreeBicategory.normalizeEquiv 📋 Mathlib.CategoryTheory.Bicategory.Coherence
  {B : Type u} [Quiver B] (a b : B) : CategoryTheory.FreeBicategory.Hom a b ≌ CategoryTheory.Discrete (Quiver.Path a b)
• CategoryTheory.FreeBicategory.normalizeAux_id 📋 Mathlib.CategoryTheory.Bicategory.Coherence
  {B : Type u} [Quiver B] {a : B} {b : CategoryTheory.FreeBicategory B} (p : Quiver.Path a b) : CategoryTheory.FreeBicategory.normalizeAux p (CategoryTheory.CategoryStruct.id b) = p
• CategoryTheory.FreeBicategory.normalizeAux_congr 📋 Mathlib.CategoryTheory.Bicategory.Coherence
  {B : Type u} [Quiver B] {a b c : B} (p : Quiver.Path a b) {f g : CategoryTheory.FreeBicategory.Hom b c} (η : f ⟶ g) : CategoryTheory.FreeBicategory.normalizeAux p f = CategoryTheory.FreeBicategory.normalizeAux p g
• CategoryTheory.FreeBicategory.normalizeAux_nil_comp 📋 Mathlib.CategoryTheory.Bicategory.Coherence
  {B : Type u} [Quiver B] {a b c : B} (f : CategoryTheory.FreeBicategory.Hom a b) (g : CategoryTheory.FreeBicategory.Hom b c) : CategoryTheory.FreeBicategory.normalizeAux Quiver.Path.nil (f.comp g) = (CategoryTheory.FreeBicategory.normalizeAux Quiver.Path.nil f).comp (CategoryTheory.FreeBicategory.normalizeAux Quiver.Path.nil g)
• CategoryTheory.FreeBicategory.normalizeAux_comp 📋 Mathlib.CategoryTheory.Bicategory.Coherence
  {B : Type u} [Quiver B] {a : B} {b c d : CategoryTheory.FreeBicategory B} (p : Quiver.Path a b) (f : b ⟶ c) (g : c ⟶ d) : CategoryTheory.FreeBicategory.normalizeAux p (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.FreeBicategory.normalizeAux (CategoryTheory.FreeBicategory.normalizeAux p f) g
• CategoryTheory.FreeBicategory.normalizeIso 📋 Mathlib.CategoryTheory.Bicategory.Coherence
  {B : Type u} [Quiver B] {a b c : B} (p : Quiver.Path a b) (f : CategoryTheory.FreeBicategory.Hom b c) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.FreeBicategory.preinclusion B).map { as := p }) f ≅ (CategoryTheory.FreeBicategory.preinclusion B).map { as := CategoryTheory.FreeBicategory.normalizeAux p f }
• CategoryTheory.FreeBicategory.normalizeIso_id 📋 Mathlib.CategoryTheory.Bicategory.Coherence
  {B : Type u} [Quiver B] {a : B} {b : CategoryTheory.FreeBicategory B} (p : Quiver.Path a b) : CategoryTheory.FreeBicategory.normalizeIso p (CategoryTheory.CategoryStruct.id b) = CategoryTheory.Bicategory.rightUnitor ((CategoryTheory.FreeBicategory.preinclusion B).map { as := p })
• CategoryTheory.FreeBicategory.inclusionMapCompAux 📋 Mathlib.CategoryTheory.Bicategory.Coherence
  {B : Type u} [Quiver B] {a b c : B} (f : Quiver.Path a b) (g : Quiver.Path b c) : (CategoryTheory.FreeBicategory.preinclusion B).map (CategoryTheory.CategoryStruct.comp { as := f } { as := g }) ≅ CategoryTheory.CategoryStruct.comp ((CategoryTheory.FreeBicategory.preinclusion B).map { as := f }) ((CategoryTheory.FreeBicategory.preinclusion B).map { as := g })
• CategoryTheory.FreeBicategory.preinclusion_map₂ 📋 Mathlib.CategoryTheory.Bicategory.Coherence
  {B : Type u} [Quiver B] {a b : B} (f g : CategoryTheory.Discrete (Quiver.Path a b)) (η : f ⟶ g) : (CategoryTheory.FreeBicategory.preinclusion B).map₂ η = CategoryTheory.eqToHom ⋯
• CategoryTheory.FreeBicategory.normalize_naturality 📋 Mathlib.CategoryTheory.Bicategory.Coherence
  {B : Type u} [Quiver B] {a b c : B} (p : Quiver.Path a b) {f g : CategoryTheory.FreeBicategory.Hom b c} (η : f ⟶ g) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft ((CategoryTheory.FreeBicategory.preinclusion B).map { as := p }) η) (CategoryTheory.FreeBicategory.normalizeIso p g).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.FreeBicategory.normalizeIso p f).hom ((CategoryTheory.FreeBicategory.preinclusion B).map₂ (CategoryTheory.eqToHom ⋯))
• CategoryTheory.FreeBicategory.normalizeIso_comp 📋 Mathlib.CategoryTheory.Bicategory.Coherence
  {B : Type u} [Quiver B] {a : B} {b c d : CategoryTheory.FreeBicategory B} (p : Quiver.Path a b) (f : b ⟶ c) (g : c ⟶ d) : CategoryTheory.FreeBicategory.normalizeIso p (CategoryTheory.CategoryStruct.comp f g) = (CategoryTheory.Bicategory.associator ((CategoryTheory.FreeBicategory.preinclusion B).map { as := p }) f g).symm ≪≫ CategoryTheory.Bicategory.whiskerRightIso (CategoryTheory.FreeBicategory.normalizeIso p f) g ≪≫ CategoryTheory.FreeBicategory.normalizeIso (CategoryTheory.FreeBicategory.normalizeAux p f) g
• CategoryTheory.Groupoid.vertexGroupIsomOfPath 📋 Mathlib.CategoryTheory.Groupoid.VertexGroup
  {C : Type u} [CategoryTheory.Groupoid C] {c d : C} (p : Quiver.Path c d) : (c ⟶ c) ≃* (d ⟶ d)
• Quiver.shortestPath 📋 Mathlib.Combinatorics.Quiver.Arborescence
  {V : Type u} [Quiver V] (r : V) [Quiver.RootedConnected r] (b : V) : Quiver.Path r b
• Quiver.Arborescence.mk 📋 Mathlib.Combinatorics.Quiver.Arborescence
  {V : Type u} [Quiver V] (root : V) (uniquePath : (b : V) → Unique (Quiver.Path root b)) : Quiver.Arborescence V
• Quiver.RootedConnected.mk 📋 Mathlib.Combinatorics.Quiver.Arborescence
  {V : Type u} [Quiver V] {r : V} (nonempty_path : ∀ (b : V), Nonempty (Quiver.Path r b)) : Quiver.RootedConnected r
• Quiver.RootedConnected.nonempty_path 📋 Mathlib.Combinatorics.Quiver.Arborescence
  {V : Type u} {inst✝ : Quiver V} {r : V} [self : Quiver.RootedConnected r] (b : V) : Nonempty (Quiver.Path r b)
• Quiver.instUniquePathRoot 📋 Mathlib.Combinatorics.Quiver.Arborescence
  {V : Type u} [Quiver V] [Quiver.Arborescence V] (b : V) : Unique (Quiver.Path (Quiver.root V) b)
• Quiver.Arborescence.uniquePath 📋 Mathlib.Combinatorics.Quiver.Arborescence
  {V : Type u} {inst✝ : Quiver V} [self : Quiver.Arborescence V] (b : V) : Unique (Quiver.Path Quiver.Arborescence.root b)
• Quiver.shortest_path_spec 📋 Mathlib.Combinatorics.Quiver.Arborescence
  {V : Type u} [Quiver V] (r : V) [Quiver.RootedConnected r] {a : V} (p : Quiver.Path r a) : (Quiver.shortestPath r a).length ≤ p.length
• Quiver.IsStronglyConnected.nonempty_path 📋 Mathlib.Combinatorics.Quiver.ConnectedComponent
  (V : Type u_2) [Quiver V] (h : Quiver.IsStronglyConnected V) (i j : V) : Nonempty (Quiver.Path i j)
• Quiver.isStronglyConnected_iff 📋 Mathlib.Combinatorics.Quiver.ConnectedComponent
  (V : Type u_2) [Quiver V] : Quiver.IsStronglyConnected V ↔ ∀ (i j : V), Nonempty (Quiver.Path i j)
• Quiver.WeaklyConnectedComponent.eq 📋 Mathlib.Combinatorics.Quiver.ConnectedComponent
  {V : Type u_1} [Quiver V] (a b : V) : Quiver.WeaklyConnectedComponent.mk a = Quiver.WeaklyConnectedComponent.mk b ↔ Nonempty (Quiver.Path a b)
• Quiver.stronglyConnectedComponent_eq_of_path 📋 Mathlib.Combinatorics.Quiver.ConnectedComponent
  {V : Type u_2} [Quiver V] {a b : V} (hab : Nonempty (Quiver.Path a b)) (hba : Nonempty (Quiver.Path b a)) : Quiver.StronglyConnectedComponent.mk a = Quiver.StronglyConnectedComponent.mk b
• Quiver.exists_path_of_stronglyConnectedComponent_eq 📋 Mathlib.Combinatorics.Quiver.ConnectedComponent
  {V : Type u_2} [Quiver V] {a b : V} (h : Quiver.StronglyConnectedComponent.mk a = Quiver.StronglyConnectedComponent.mk b) : Nonempty (Quiver.Path a b) ∧ Nonempty (Quiver.Path b a)
• Quiver.StronglyConnectedComponent.eq 📋 Mathlib.Combinatorics.Quiver.ConnectedComponent
  {V : Type u_2} [Quiver V] (a b : V) : Quiver.StronglyConnectedComponent.mk a = Quiver.StronglyConnectedComponent.mk b ↔ Nonempty (Quiver.Path a b) ∧ Nonempty (Quiver.Path b a)
• Quiver.StronglyConnectedComponent.mk_eq_mk 📋 Mathlib.Combinatorics.Quiver.ConnectedComponent
  {V : Type u_2} [Quiver V] {a b : V} : Quiver.StronglyConnectedComponent.mk a = Quiver.StronglyConnectedComponent.mk b ↔ Nonempty (Quiver.Path a b) ∧ Nonempty (Quiver.Path b a)
• Quiver.IsSStronglyConnected.exists_pos_cycle 📋 Mathlib.Combinatorics.Quiver.ConnectedComponent
  (V : Type u_2) [Quiver V] (h : Quiver.IsSStronglyConnected V) (i : V) : ∃ p, 0 < p.length
• Quiver.StronglyConnectedComponent.IsSStronglyConnected.pos_cycle 📋 Mathlib.Combinatorics.Quiver.ConnectedComponent
  {V : Type u_2} [Quiver V] (h : Quiver.IsSStronglyConnected V) (v : V) : ∃ p, 0 < p.length
• Quiver.IsSStronglyConnected.exists_pos_path 📋 Mathlib.Combinatorics.Quiver.ConnectedComponent
  (V : Type u_2) [Quiver V] (h : Quiver.IsSStronglyConnected V) (i j : V) : ∃ p, 0 < p.length
• Quiver.isSStronglyConnected_iff 📋 Mathlib.Combinatorics.Quiver.ConnectedComponent
  (V : Type u_2) [Quiver V] : Quiver.IsSStronglyConnected V ↔ ∀ (i j : V), ∃ p, 0 < p.length
• Quiver.stronglyConnectedComponent_singleton_iff 📋 Mathlib.Combinatorics.Quiver.ConnectedComponent
  {V : Type u_2} [Quiver V] (v : V) : (∀ (w : V), Quiver.StronglyConnectedComponent.mk w = Quiver.StronglyConnectedComponent.mk v → w = v) ↔ ∀ (w : V), w ≠ v → ¬(Nonempty (Quiver.Path v w) ∧ Nonempty (Quiver.Path w v))
• Quiver.PathStar.mk 📋 Mathlib.Combinatorics.Quiver.Covering
  {U : Type u_1} [Quiver U] {u v : U} (p : Quiver.Path u v) : Quiver.PathStar u
• Prefunctor.pathStar_apply 📋 Mathlib.Combinatorics.Quiver.Covering
  {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] (φ : U ⥤q V) {u v : U} (p : Quiver.Path u v) : φ.pathStar u (Quiver.PathStar.mk p) = Quiver.PathStar.mk (φ.mapPath p)
• Quiver.Path.exists_mem_notMem_hom_path_path_of_notMem_mem 📋 Mathlib.Combinatorics.Quiver.Path.Decomposition
  {V : Type u_1} [Quiver V] {a b : V} (p : Quiver.Path a b) (S : Set V) (ha_in_S : a ∈ S) (hb_not_in_S : b ∉ S) : ∃ u ∈ S, ∃ v ∉ S, ∃ e p₁ p₂, p = p₁.comp (e.toPath.comp p₂)
• Quiver.Path.exists_notMem_mem_hom_path_path_of_notMem_mem 📋 Mathlib.Combinatorics.Quiver.Path.Decomposition
  {V : Type u_1} [Quiver V] {a b : V} (p : Quiver.Path a b) (S : Set V) (ha_not_in_S : a ∉ S) (hb_in_S : b ∈ S) : ∃ u ∉ S, ∃ v ∈ S, ∃ e p₁ p₂, p = p₁.comp (e.toPath.comp p₂)
• Quiver.Path.end 📋 Mathlib.Combinatorics.Quiver.Path.Vertices
  {V : Type u_1} [Quiver V] {a b : V} : Quiver.Path a b → V
• Quiver.Path.vertices 📋 Mathlib.Combinatorics.Quiver.Path.Vertices
  {V : Type u_1} [Quiver V] {a b : V} : Quiver.Path a b → List V
• Quiver.Path.vertices_ne_nil 📋 Mathlib.Combinatorics.Quiver.Path.Vertices
  {V : Type u_1} [Quiver V] {a b : V} (p : Quiver.Path a b) : p.vertices ≠ []
• Quiver.Path.end_mem_vertices 📋 Mathlib.Combinatorics.Quiver.Path.Vertices
  {V : Type u_1} [Quiver V] {a b : V} (p : Quiver.Path a b) : b ∈ p.vertices
• Quiver.Path.start_mem_vertices 📋 Mathlib.Combinatorics.Quiver.Path.Vertices
  {V : Type u_1} [Quiver V] {a b : V} (p : Quiver.Path a b) : a ∈ p.vertices
• Quiver.Path.vertices_head? 📋 Mathlib.Combinatorics.Quiver.Path.Vertices
  {V : Type u_1} [Quiver V] {a b : V} (p : Quiver.Path a b) : p.vertices.head? = some a
• Quiver.Path.length_vertices_pos 📋 Mathlib.Combinatorics.Quiver.Path.Vertices
  {V : Type u_1} [Quiver V] {a b : V} (p : Quiver.Path a b) : 0 < p.vertices.length
• Quiver.Path.end_cons 📋 Mathlib.Combinatorics.Quiver.Path.Vertices
  {V : Type u_1} [Quiver V] {a b c : V} (p : Quiver.Path a b) (e : b ⟶ c) : (p.cons e).end = c
• Quiver.Path.length_eq_zero_iff 📋 Mathlib.Combinatorics.Quiver.Path.Vertices
  {V : Type u_1} [Quiver V] {a : V} (p : Quiver.Path a a) : p.length = 0 ↔ p = Quiver.Path.nil
• Quiver.Path.vertices_length 📋 Mathlib.Combinatorics.Quiver.Path.Vertices
  {V : Type u_2} [Quiver V] {a b : V} (p : Quiver.Path a b) : p.vertices.length = p.length + 1
• Quiver.Path.vertices_getLast 📋 Mathlib.Combinatorics.Quiver.Path.Vertices
  {V : Type u_1} [Quiver V] {a b : V} (p : Quiver.Path a b) (h : p.vertices ≠ [] := ⋯) : p.vertices.getLast h = b
• Quiver.Path.vertices_head_eq 📋 Mathlib.Combinatorics.Quiver.Path.Vertices
  {V : Type u_1} [Quiver V] {a b : V} (p : Quiver.Path a b) (h : p.vertices ≠ [] := ⋯) : p.vertices.head h = a
• Quiver.Path.vertices_cons 📋 Mathlib.Combinatorics.Quiver.Path.Vertices
  {V : Type u_1} [Quiver V] {a b c : V} (p : Quiver.Path a b) (e : b ⟶ c) : (p.cons e).vertices = p.vertices.concat c
• Quiver.Path.dropLast_append_end_eq 📋 Mathlib.Combinatorics.Quiver.Path.Vertices
  {V : Type u_1} [Quiver V] {a b : V} (p : Quiver.Path a b) : p.vertices.dropLast ++ [b] = p.vertices
• Quiver.Path.nil_of_comp_eq_nil_left 📋 Mathlib.Combinatorics.Quiver.Path.Vertices
  {V : Type u_1} [Quiver V] {a b : V} {p : Quiver.Path a b} {q : Quiver.Path b a} (h : p.comp q = Quiver.Path.nil) : p.length = 0
• Quiver.Path.nil_of_comp_eq_nil_right 📋 Mathlib.Combinatorics.Quiver.Path.Vertices
  {V : Type u_1} [Quiver V] {a b : V} {p : Quiver.Path a b} {q : Quiver.Path b a} (h : p.comp q = Quiver.Path.nil) : q.length = 0
• Quiver.Path.getElem_vertices_zero 📋 Mathlib.Combinatorics.Quiver.Path.Vertices
  {V : Type u_1} [Quiver V] {a b : V} (p : Quiver.Path a b) : p.vertices[0] = a
• Quiver.Path.mem_vertices_cons 📋 Mathlib.Combinatorics.Quiver.Path.Vertices
  {V : Type u_1} [Quiver V] {a b c : V} (p : Quiver.Path a b) (e : b ⟶ c) {x : V} : x ∈ (p.cons e).vertices ↔ x ∈ p.vertices ∨ x = c
• Quiver.Path.vertices_comp 📋 Mathlib.Combinatorics.Quiver.Path.Vertices
  {V : Type u_1} [Quiver V] {a b c : V} (p : Quiver.Path a b) (q : Quiver.Path b c) : (p.comp q).vertices = p.vertices.dropLast ++ q.vertices
• Quiver.Path.comp_eq_nil_iff 📋 Mathlib.Combinatorics.Quiver.Path.Vertices
  {V : Type u_1} [Quiver V] {a b : V} {p : Quiver.Path a b} {q : Quiver.Path b a} : p.comp q = Quiver.Path.nil ↔ p.length = 0 ∧ q.length = 0
• Quiver.Path.exists_eq_comp_of_mem_vertices 📋 Mathlib.Combinatorics.Quiver.Path.Vertices
  {V : Type u_1} [Quiver V] {a b : V} (p : Quiver.Path a b) {v : V} (hv : v ∈ p.vertices) : ∃ p₁ p₂, p = p₁.comp p₂
• Quiver.Path.exists_eq_comp_of_le_length 📋 Mathlib.Combinatorics.Quiver.Path.Vertices
  {V : Type u_1} [Quiver V] {a b : V} (p : Quiver.Path a b) {n : ℕ} (hn : n ≤ p.length) : ∃ v p₁ p₂, p = p₁.comp p₂ ∧ p₁.length = n
• Quiver.Path.exists_eq_comp_and_notMem_tail_of_mem_vertices 📋 Mathlib.Combinatorics.Quiver.Path.Vertices
  {V : Type u_1} [Quiver V] {a b : V} (p : Quiver.Path a b) {v : V} (hv : v ∈ p.vertices) : ∃ p₁ p₂, p = p₁.comp p₂ ∧ v ∉ p₂.vertices.tail
• Quiver.Path.vertices_comp_get_length_eq 📋 Mathlib.Combinatorics.Quiver.Path.Vertices
  {V : Type u_1} [Quiver V] {a b c : V} (p₁ : Quiver.Path a c) (p₂ : Quiver.Path c b) (h : p₁.length < (p₁.comp p₂).vertices.length := by simp) : (p₁.comp p₂).vertices.get ⟨p₁.length, h⟩ = c
• Quiver.Path.exists_eq_comp_and_length_eq_of_lt_length 📋 Mathlib.Combinatorics.Quiver.Path.Vertices
  {V : Type u_1} [Quiver V] {a b : V} (p : Quiver.Path a b) (n : ℕ) (hn : n < p.vertices.length) : ∃ v p₁ p₂, p = p₁.comp p₂ ∧ p₁.length = n ∧ v = p.vertices[n]
• Quiver.Path.addWeightOfEPs 📋 Mathlib.Combinatorics.Quiver.Path.Weight
  {V : Type u_1} [Quiver V] {R : Type u_2} [AddMonoid R] (w : V → V → R) {i j : V} : Quiver.Path i j → R
• Quiver.Path.weightOfEPs 📋 Mathlib.Combinatorics.Quiver.Path.Weight
  {V : Type u_1} [Quiver V] {R : Type u_2} [Monoid R] (w : V → V → R) {i j : V} : Quiver.Path i j → R
• Quiver.Path.addWeight 📋 Mathlib.Combinatorics.Quiver.Path.Weight
  {V : Type u_1} [Quiver V] {R : Type u_3} [AddMonoid R] (w : {i j : V} → (i ⟶ j) → R) {i j : V} : Quiver.Path i j → R
• Quiver.Path.weight 📋 Mathlib.Combinatorics.Quiver.Path.Weight
  {V : Type u_1} [Quiver V] {R : Type u_2} [Monoid R] (w : {i j : V} → (i ⟶ j) → R) {i j : V} : Quiver.Path i j → R
• Quiver.Path.addWeightOfEPs_cons 📋 Mathlib.Combinatorics.Quiver.Path.Weight
  {V : Type u_1} [Quiver V] {R : Type u_2} [AddMonoid R] (w : V → V → R) {a b c : V} (p : Quiver.Path a b) (e : b ⟶ c) : Quiver.Path.addWeightOfEPs w (p.cons e) = Quiver.Path.addWeightOfEPs w p + w b c
• Quiver.Path.weightOfEPs_cons 📋 Mathlib.Combinatorics.Quiver.Path.Weight
  {V : Type u_1} [Quiver V] {R : Type u_2} [Monoid R] (w : V → V → R) {a b c : V} (p : Quiver.Path a b) (e : b ⟶ c) : Quiver.Path.weightOfEPs w (p.cons e) = Quiver.Path.weightOfEPs w p * w b c
• Quiver.Path.addWeightOfEPs_comp 📋 Mathlib.Combinatorics.Quiver.Path.Weight
  {V : Type u_1} [Quiver V] {R : Type u_2} [AddMonoid R] (w : V → V → R) {a b c : V} (p : Quiver.Path a b) (q : Quiver.Path b c) : Quiver.Path.addWeightOfEPs w (p.comp q) = Quiver.Path.addWeightOfEPs w p + Quiver.Path.addWeightOfEPs w q
• Quiver.Path.weightOfEPs_comp 📋 Mathlib.Combinatorics.Quiver.Path.Weight
  {V : Type u_1} [Quiver V] {R : Type u_2} [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
• Quiver.Path.addWeight_cons 📋 Mathlib.Combinatorics.Quiver.Path.Weight
  {V : Type u_1} [Quiver V] {R : Type u_2} [AddMonoid R] (w : {i j : V} → (i ⟶ j) → R) {a b c : V} (p : Quiver.Path a b) (e : b ⟶ c) : Quiver.Path.addWeight (fun {i j} => w) (p.cons e) = Quiver.Path.addWeight (fun {i j} => w) p + w e
• Quiver.Path.weight_cons 📋 Mathlib.Combinatorics.Quiver.Path.Weight
  {V : Type u_1} [Quiver V] {R : Type u_2} [Monoid R] (w : {i j : V} → (i ⟶ j) → R) {a b c : V} (p : Quiver.Path a b) (e : b ⟶ c) : Quiver.Path.weight (fun {i j} => w) (p.cons e) = Quiver.Path.weight (fun {i j} => w) p * w e
• Quiver.Path.addWeight_comp 📋 Mathlib.Combinatorics.Quiver.Path.Weight
  {V : Type u_1} [Quiver V] {R : Type u_2} [AddMonoid R] (w : {i j : V} → (i ⟶ j) → R) {a b c : V} (p : Quiver.Path a b) (q : Quiver.Path b c) : Quiver.Path.addWeight (fun {i j} => w) (p.comp q) = Quiver.Path.addWeight (fun {i j} => w) p + Quiver.Path.addWeight (fun {i j} => w) q
• Quiver.Path.weight_comp 📋 Mathlib.Combinatorics.Quiver.Path.Weight
  {V : Type u_1} [Quiver V] {R : Type u_2} [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
• Quiver.Path.weightOfEPs_nonneg 📋 Mathlib.Combinatorics.Quiver.Path.Weight
  {V : Type u_1} [Quiver V] {R : Type u_2} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] {w : V → V → R} (hw : ∀ (i j : V), 0 ≤ w i j) {i j : V} (p : Quiver.Path i j) : 0 ≤ Quiver.Path.weightOfEPs w p
• Quiver.Path.weightOfEPs_pos 📋 Mathlib.Combinatorics.Quiver.Path.Weight
  {V : Type u_1} [Quiver V] {R : Type u_2} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] {w : V → V → R} (hw : ∀ (i j : V), 0 < w i j) {i j : V} (p : Quiver.Path i j) : 0 < Quiver.Path.weightOfEPs w p
• Quiver.Path.weight_nonneg 📋 Mathlib.Combinatorics.Quiver.Path.Weight
  {V : Type u_1} [Quiver V] {R : Type u_2} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] {w : {i j : V} → (i ⟶ j) → R} (hw : ∀ {i j : V} (e : i ⟶ j), 0 ≤ w e) {i j : V} (p : Quiver.Path i j) : 0 ≤ Quiver.Path.weight (fun {i j} => w) p
• Quiver.Path.weight_pos 📋 Mathlib.Combinatorics.Quiver.Path.Weight
  {V : Type u_1} [Quiver V] {R : Type u_2} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] {w : {i j : V} → (i ⟶ j) → R} (hw : ∀ {i j : V} (e : i ⟶ j), 0 < w e) {i j : V} (p : Quiver.Path i j) : 0 < Quiver.Path.weight (fun {i j} => w) p
• IsFreeGroupoid.path_nonempty_of_hom 📋 Mathlib.GroupTheory.FreeGroup.NielsenSchreier
  {G : Type u} [CategoryTheory.Groupoid G] [IsFreeGroupoid G] {a b : G} : Nonempty (a ⟶ b) → Nonempty (Quiver.Path (IsFreeGroupoid.symgen✝ a) (IsFreeGroupoid.symgen✝ b))
• IsFreeGroupoid.SpanningTree.homOfPath 📋 Mathlib.GroupTheory.FreeGroup.NielsenSchreier
  {G : Type u} [CategoryTheory.Groupoid G] [IsFreeGroupoid G] (T : WideSubquiver (Quiver.Symmetrify (IsFreeGroupoid.Generators G))) [Quiver.Arborescence (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)] {a : G} : Quiver.Path (Quiver.root (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)) a → (IsFreeGroupoid.SpanningTree.root'✝ T ⟶ a)
• IsFreeGroupoid.SpanningTree.treeHom_eq 📋 Mathlib.GroupTheory.FreeGroup.NielsenSchreier
  {G : Type u} [CategoryTheory.Groupoid G] [IsFreeGroupoid G] (T : WideSubquiver (Quiver.Symmetrify (IsFreeGroupoid.Generators G))) [Quiver.Arborescence (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)] {a : G} (p : Quiver.Path (Quiver.root (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)) a) : IsFreeGroupoid.SpanningTree.treeHom T a = IsFreeGroupoid.SpanningTree.homOfPath T p
• Matrix.transposePath 📋 Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
  {n : Type u_1} {R : Type u_2} [Ring R] [LinearOrder R] {A : Matrix n n R} {i j : n} (p : Quiver.Path i j) : Quiver.Path j i
• Matrix.pow_apply_pos_iff_nonempty_path 📋 Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
  {n : Type u_1} {R : Type u_2} [Ring R] [LinearOrder R] {A : Matrix n n R} [Fintype n] [IsOrderedRing R] [PosMulStrictMono R] [Nontrivial R] [DecidableEq n] (hA : ∀ (i j : n), 0 ≤ A i j) (k : ℕ) (i j : n) : 0 < (A ^ k) i j ↔ Nonempty { p // p.length = k }

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision 01cceef