FMLJohn

Stream: new members

[FMLJohn]

Hello! Jujian Zhang and I have formalized in lean 4 some stuff in dimension theory. We have defined the Krull dimension of a commutative ring and a topological space. Here are some of the results we have formalized: for a commutative ring, its topological Krull dimension is the same as its ring-theoretical Krull dimension; if I is a prime ideal of a commutative ring R, then the height of I is equal to the Krull dimension of the localization of R with respect to I; the Krull dimension of a non-field PID is 1, etc. But most of what we have formalized have not been put into Mathlib 4 yet.

[Notification Bot]

A message was moved here from #new members > Isaiah Mindich by Johan Commelin.

[Johan Commelin]

Nice work! (I moved your message to a new thread.)

[Patrick Massot]

Are you also working with Kevin?