Mathlib Map

Theorems · Inductive type · commutative algebra

CommRingCat

Type (u + 1)

The category of commutative rings.

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

Around this declaration

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

AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace · cited by 1892LocallyRingedSpace.toShea…CommRingCat.carrier · cited by 1096CommRingCat.carrierAlgebraicGeometry.LocallyRingedSpace.Hom.toHom · cited by 995Hom.toHomAlgebraicGeometry.Spec · cited by 626AlgebraicGeometry.SpecCommRingCat.Hom.hom · cited by 432Hom.homAlgebraicGeometry.Spec.map · cited by 332Spec.mapCommRingCat.ofHom · cited by 259CommRingCat.ofHomAlgebraicGeometry.Scheme.Hom.opensFunctor · cited by 204Hom.opensFunctorAlgebraicGeometry.Scheme.Hom.app · cited by 176Hom.appAlgebraicGeometry.Scheme.basicOpen · cited by 141Scheme.basicOpenAlgebraicGeometry.Scheme.Hom.appLE · cited by 138Hom.appLEAlgebraicGeometry.Scheme.Hom.appTop · cited by 109Hom.appTopAlgebraicGeometry.Scheme.ΓSpecIso · cited by 106Scheme.ΓSpecIsoAlgebraicGeometry.Scheme.homOfLE · cited by 103Scheme.homOfLEAlgebraicGeometry.Scheme.residueField · cited by 95Scheme.residueFieldCommRingCatCITED BYCITES

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 by3,003

Results whose statement or proof uses this declaration.

Showing the 200 most cited of 3,003.