Theorems · Definition · category theory
FintypeCat
Type (u_1 + 1)
The category of finite types.
- Defined in
- Mathlib.CategoryTheory.FintypeCat
- Cited by
- 217 results in Mathlib
- Foundations
- Depth 11 from the axioms, rests on 54 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finiteproof · cited by 3,029
- CategoryTheory.ObjectProperty.FullSubcategoryproof · cited by 726
Cited by350
Results whose statement or proof uses this declaration.
- CategoryTheory.PreGaloisCategory.FiberFunctorstatement · cited by 66
- CategoryTheory.PreGaloisCategory.PointedGaloisObjectstatement · cited by 34
- FintypeCat.toProfinitestatement and proof · cited by 32
- CategoryTheory.PreGaloisCategory.PointedGaloisObject.objstatement and proof · cited by 29
- FintypeCat.ofstatement · cited by 26
- FintypeCat.toLightProfinitestatement and proof · cited by 23
- CategoryTheory.PreGaloisCategory.PointedGaloisObject.ptstatement and proof · cited by 16
- FintypeCat.inclstatement · cited by 16
- CategoryTheory.PreGaloisCategory.AutGaloisstatement and proof · cited by 12
- Action.FintypeCat.ofMulActionstatement and proof · cited by 11
- CategoryTheory.Matproof · cited by 11
- CategoryTheory.PreGaloisCategory.PointedGaloisObject.Hom.valstatement and proof · cited by 11
Showing the 200 most cited of 350.