Zulip Chat Archive

Stream: Is there code for X?

Topic: IsNoetherianRing → Ideal.FiniteHeight

Jz Pan (Mar 28 2025 at 15:11):

This is claimed at the docstring of docs#Ideal.FiniteHeight but seems that there is no proof in mathlib yet.

Jz Pan (Mar 28 2025 at 15:12):

@loogle |- Ideal.FiniteHeight ..

loogle (Mar 28 2025 at 15:12):

:search: Ideal.finiteHeight_of_finiteRingKrullDim, Ideal.FiniteHeight.mk, and 1 more

Christian Merten (Mar 29 2025 at 00:12):

This will follow from Krull's height theorem, which is being ported to Lean 4, but which still takes time.

Jz Pan (Mar 29 2025 at 04:36):

I see. What's the PR of it?

Andrew Yang (Mar 31 2025 at 07:56):

It is #22403

Last updated: May 02 2025 at 03:31 UTC