Structures · Algebra
IsRegularLocalRing
A Noetherian local ring is said to be regular if its maximal ideal
can be generated by dim R elements.
- Defined in
- Mathlib.RingTheory.RegularLocalRing.Defs
- Shape
- One type argument · adds spanFinrank_maximalIdeal
Extends2
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- Localization.AtPrime
How is a type an instance?
Loading the hierarchy index…