Mathlib Map

Theorems · Definition · category theory

CategoryTheory.isIsomorphicSetoid

(C : Type u) → [CategoryTheory.Category.{v, u} C] → Setoid C

IsIsomorphic defines a setoid.

Defined in
Mathlib.CategoryTheory.IsomorphismClasses
Cited by
24 results in Mathlib
Foundations
Depth 17 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
CategoryTheory.Category
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

CommRing.Pic.mk · cited by 17Pic.mkCategoryTheory.ThinSkeleton · cited by 17CategoryTheory.ThinSkelet…CategoryTheory.toSkeleton · cited by 10CategoryTheory.toSkeletonCategoryTheory.ThinSkeleton.map · cited by 6ThinSkeleton.mapCategoryTheory.ThinSkeleton.skeletal · cited by 5ThinSkeleton.skeletalCommRing.Pic.mk_eq_iff · cited by 5Pic.mk_eq_iffCommRing.Pic.mk_eq_self · cited by 5Pic.mk_eq_selfCommRing.Pic.mk.linearEquiv · cited by 3mk.linearEquivCategoryTheory.Subobject.inf_eq_map_pullback' · cited by 3Subobject.inf_eq_map_pull…CategoryTheory.ThinSkeleton.fromThinSkeleton · cited by 3ThinSkeleton.fromThinSkel…CategoryTheory.ThinSkeleton.map₂Functor · cited by 2ThinSkeleton.map₂FunctorCommRing.Pic.mk_tensor · cited by 2Pic.mk_tensorCategoryTheory.ThinSkeleton.map₂NatTrans · cited by 1ThinSkeleton.map₂NatTransCommRing.Pic.mk_dual · cited by 1Pic.mk_dualSubmodule.unitsToPicEquiv · cited by 1Submodule.unitsToPicEquivCategoryTheory.Category · cited by 32673CategoryTheory.CategoryCategoryTheory.IsIsomorphic · cited by 9CategoryTheory.IsIsomorph…CategoryTheory.isIsomorphicSe…CITED BYCITES

Cites2

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

Cited by34

Results whose statement or proof uses this declaration.