Theorems · Theorem · combinatorics

Quiver.Symmetrify.lift_spec

∀ {V : Type u_2} [inst : Quiver V] {V' : Type u_4} [inst_1 : Quiver V'] [inst_2 : Quiver.HasReverse V'] (φ : V ⥤q V'),
  Quiver.Symmetrify.of ⋙q Quiver.Symmetrify.lift φ = φ

Defined in

Mathlib.Combinatorics.Quiver.Symmetric

Cited by

1 results in Mathlib

Foundations

Depth 6 from the axioms · uses Quot.sound

Assumes

QuiverQuiverQuiver.HasReverse