The predicate records equality of the Krull dimension and the depth of the ring with a specified natural number. Its two projections recover the dimension and depth equalities.
The local ring has Krull dimension and module depth both equal to d.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace IsLocalRing
variable (R : Type*) [CommRing R] [IsLocalRing R]def IsCohenMacaulayOfDim (d : ℕ) : PropSurrounding namespaces, section variables, and local commands at this declaration.
namespace IsLocalRing
variable (R : Type*) [CommRing R] [IsLocalRing R]
namespace IsCohenMacaulayOfDim
variable {R} {d : ℕ}lemma ringKrullDim_eq (h : IsCohenMacaulayOfDim R d) : ringKrullDim R = dSurrounding namespaces, section variables, and local commands at this declaration.
namespace IsLocalRing
variable (R : Type*) [CommRing R] [IsLocalRing R]
namespace IsCohenMacaulayOfDim
variable {R} {d : ℕ}lemma depth_eq (h : IsCohenMacaulayOfDim R d) : Module.depth R R = d