Theorems · Definition · category theory
GrpCat.carrier
GrpCat → Type u
The underlying type.
- Defined in
- Mathlib.Algebra.Category.Grp.Basic
- Cited by
- 125 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 2 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- GrpCatstatement and proof · cited by 146
Cited by195
Results whose statement or proof uses this declaration.
- GrpCat.Hom.homstatement · cited by 47
- CategoryTheory.PresheafOfGroups.OneCochain.evstatement · cited by 15
- GrpCat.SurjectiveOfEpiAuxs.gstatement and proof · cited by 8
- CategoryTheory.PresheafOfGroups.ZeroCochainproof · cited by 7
- GrpCat.SurjectiveOfEpiAuxs.hstatement and proof · cited by 7
- GrpCat.shrinkFunctorstatement and proof · cited by 6
- GrpCat.FilteredColimits.G.mkstatement and proof · cited by 5
- GrpCat.toAddGrpproof · cited by 4
- MulEquiv.toGrpIsostatement and proof · cited by 4
- CategoryTheory.GrpObj.ofRepresentableBystatement · cited by 4
- GrpCat.SurjectiveOfEpiAuxs.fromCoset_eq_of_mem_rangestatement and proof · cited by 3
- GrpCat.SurjectiveOfEpiAuxs.fromCoset_ne_of_nin_rangestatement and proof · cited by 3