Krull dimension, regular rings

Stream: Is there code for X?

[Jon Eugster]

Is there an implementation of regular (local) rings?

This would likely import ring_theory.noetherian or have some mentioning of "Krull dimension", both searches didn't lead anywhere. Krull dimension seems only been used in cases where it's $\le 1$ (e.g. dedekin domain, PID).

[Johan Commelin]

I don't think this is in mathlib yet. @Filippo A. E. Nuccio @Anne Baanen did you define Krull dimension in your project?

[Johan Commelin]

It would certainly be a natural and welcome addition to mathlib at this point

[Filippo A. E. Nuccio]

No, we just say what it means to have Krull dimension less or equal to one (every non-zero prime is maximal). But we don't speak about chains of ideals.

[Jon Eugster]

thank you!
@Johan Commelin Out of interest (to get more familiar with the mathlib structure), where would you put this? Are you generally making new files for each property a ring can have, like regular, normal, complete intersection etc. or are you bundling those as they kinda form a hierarchy of properties?

[Johan Commelin]

There is not a very strict rule here. Files >1000 tend to get split up. Files with <100 lines are not a problem at all.

[Johan Commelin]

So if it's really a new topic, I would start a new file

[Johan Commelin]

src/ring_theory/regular.lean looks good to me