Mathlib Map

Theorems · Definition · commutative algebra

RingCat.carrier

RingCat → Type u

The underlying type.

Defined in
Mathlib.Algebra.Category.Ring.Basic
Cited by
279 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.

PresheafOfModules.obj · cited by 186PresheafOfModules.objPresheafOfModules.Hom.app · cited by 88Hom.appPresheafOfModules.presheaf · cited by 85PresheafOfModules.presheafRingCat.Hom.hom · cited by 85Hom.homPresheafOfModules.map · cited by 55PresheafOfModules.mapAlgebraicGeometry.Scheme.Modules.Hom.app · cited by 26Hom.appPresheafOfModules.Derivation · cited by 18PresheafOfModules.Derivat…PresheafOfModules.evaluation · cited by 17PresheafOfModules.evaluat…PresheafOfModules.Submodule.obj · cited by 15Submodule.objPresheafOfModules.hom_ext · cited by 14PresheafOfModules.hom_extPresheafOfModules.ModuleColimit.ιM · cited by 12ModuleColimit.ιMSheafOfModules.evaluation · cited by 11SheafOfModules.evaluationSheafOfModules.Presentation.relations · cited by 10Presentation.relationsPresheafOfModules.Derivation.d · cited by 10Derivation.dPresheafOfModules.Sheafify.smul · cited by 9Sheafify.smulRingCat · cited by 473RingCatRingCat.carrierCITED BYCITES

Cites1

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

  • RingCatstatement and proof · cited by 473

Cited by450

Results whose statement or proof uses this declaration.

Showing the 200 most cited of 450.