Theorems · Inductive type · commutative algebra
RingCat
Type (u + 1)
The category of rings.
- Defined in
- Mathlib.Algebra.Category.Ring.Basic
- Cited by
- 473 results in Mathlib
- Foundations
- Depth 0 from the axioms, rests on 1 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by894
Results whose statement or proof uses this declaration.
- RingCat.carrierstatement and proof · cited by 279
- PresheafOfModulesstatement · cited by 247
- SheafOfModulesstatement · cited by 188
- PresheafOfModules.objstatement and proof · cited by 186
- PresheafOfModules.Hom.appstatement and proof · cited by 88
- RingCat.Hom.homstatement and proof · cited by 85
- PresheafOfModules.presheafstatement and proof · cited by 85
- SheafOfModules.freestatement and proof · cited by 60
- PresheafOfModules.mapstatement and proof · cited by 55
- SheafOfModules.valstatement and proof · cited by 55
- SheafOfModules.pushforwardstatement and proof · cited by 45
- SheafOfModules.unitstatement and proof · cited by 45
Showing the 200 most cited of 894.