Mathlib Map

Structures · Algebra

IsRegularRing

A noetherian ring is regular if its localization at any prime IsRegularLocalRing.

Defined in
Mathlib.RingTheory.RegularLocalRing.Defs
Shape
One type argument · adds isRegularLocalRing_localization

Extends1

Extended by0

Nothing extends this class yet.

Concrete types that are instances2

  • Polynomial
  • MvPolynomial

How is a type an instance?

Loading the hierarchy index…

Assumed by6

Ancestors1