Theorems · Definition · commutative algebra
CommRingCat.carrier
CommRingCat → Type u
The underlying type.
- Defined in
- Mathlib.Algebra.Category.Ring.Basic
- Cited by
- 1,096 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.
- CommRingCatstatement and proof · cited by 2,333
Cited by1,397
Results whose statement or proof uses this declaration.
- CommRingCat.Hom.homstatement · cited by 432
- AlgebraicGeometry.Scheme.basicOpenstatement and proof · cited by 141
- AlgebraicGeometry.Scheme.residueFieldproof · cited by 95
- AlgebraicGeometry.Scheme.IdealSheafData.idealstatement · cited by 88
- AlgebraicGeometry.Scheme.zeroLocusstatement and proof · cited by 60
- CommRingCat.hom_extstatement · cited by 55
- CategoryTheory.Iso.commRingCatIsoToRingEquivstatement · cited by 44
- AlgebraicGeometry.Scheme.basicOpen_lestatement and proof · cited by 43
- AlgebraicGeometry.RingedSpace.basicOpenstatement and proof · cited by 30
- AlgebraicGeometry.Scheme.Hom.toNormalizationproof · cited by 28
- CommRingCat.Hom.hom'statement · cited by 27
- CommRingCat.hom_compstatement · cited by 27
Showing the 200 most cited of 1,397.