Noether normalization

Stream: Is there code for X?

[Yongle Hu]

Hi! Is there a formalization of Noether normalization in Mathlib now? I have found Hilber Nullstellensatz MvPolynomial.vanishingIdeal_zeroLocus_eq_radical, but I found the proof of Hilber Nullstellensatz in Mathlib is not rely on Noether normalization, and I don't find any relative theorem of Nother normalization in Mahtlib.

[Johan Commelin]

I'm quite sure we don't have it. I would expect to find a match in the following results otherwise:

@loogle MvPolynomial, Module.Finite

[Johan Commelin]

@loogle MvPolynomial, Module.Finite

[loogle]

:search: LinearMap.polyCharpoly, LinearMap.polyCharpoly_monic, and 27 more

[Johan Commelin]

But none of the results look anything like Noether normalization