Mathlib Map

Theorems · Definition · category theory

AddCommGrpCat.carrier

AddCommGrpCat → Type u

The underlying type.

Defined in
Mathlib.Algebra.Category.Grp.Basic
Cited by
407 results in Mathlib
Foundations
Depth 1 from the axioms, rests on 2 definitions · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

AddCommGrpCat.Hom.hom · cited by 72Hom.homSheafOfModules.free · cited by 60SheafOfModules.freeSheafOfModules.GeneratingSections.I · cited by 28GeneratingSections.ISheafOfModules.GeneratingSections · cited by 27SheafOfModules.Generating…SheafOfModules.Presentation · cited by 24SheafOfModules.Presentati…PresheafOfModules.ModuleColimit · cited by 22PresheafOfModules.ModuleC…SheafOfModules.GeneratingSections.π · cited by 20GeneratingSections.πSheafOfModules.freeHomEquiv · cited by 20SheafOfModules.freeHomEqu…AddCommGrpCat.Colimits.Quot · cited by 16Colimits.QuotSheafOfModules.QuasicoherentData · cited by 16SheafOfModules.Quasicoher…SheafOfModules.ιFree · cited by 15SheafOfModules.ιFreeSheafOfModules.Presentation.generators · cited by 14Presentation.generatorsSheafOfModules.LocalGeneratorsData · cited by 14SheafOfModules.LocalGener…AddCommGrpCat.hom_ext · cited by 13AddCommGrpCat.hom_extModuleCat.smul · cited by 13ModuleCat.smulAddCommGrpCat · cited by 462AddCommGrpCatAddCommGrpCat.carrierCITED BYCITES

Cites1

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

Cited by628

Results whose statement or proof uses this declaration.

Showing the 200 most cited of 628.