Theorems · Theorem · category theory
CategoryTheory.Quiv.homEquivOfIso_symm_apply
∀ {V W : CategoryTheory.Quiv} (e : V ≅ W) {X Y : ↑V} (g : e.hom.obj X ⟶ e.hom.obj Y),
(CategoryTheory.Quiv.homEquivOfIso e).symm g = Quiver.homOfEq (e.inv.map g) ⋯ ⋯- Defined in
- Mathlib.CategoryTheory.Category.Quiv
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 19 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Quiver.Homstatement and proof · cited by 32,603
- Equivstatement · cited by 8,337
- CategoryTheory.Iso.homstatement and proof · cited by 7,684
- CategoryTheory.Iso.invstatement · cited by 6,514
- CategoryTheory.Isostatement and proof · cited by 3,963
- Equiv.symmstatement and proof · cited by 3,681
- Prefunctor.objstatement and proof · cited by 1,241
- Prefunctor.mapstatement · cited by 952
- CategoryTheory.Bundled.αstatement and proof · cited by 736
- Quiverstatement · cited by 405
- CategoryTheory.Quivstatement and proof · cited by 21
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.