Commit 2026-10-17 12:17 7a4ff2c0

chore(RingTheory): delete outdated proof_wanted (#42649) MvPolynomial.ringKrullDim_of_isNoetherianRing was added two years after this proof_wanted and is nearly identical. The difference is that it is defined for arbitrary index sets instead of Fin and for CommRing instead of CommSemiring. This is an artifact of Ideal.height being defined for CommRings and ringKrullDim for CommSemirings. Otherwise I think the original intention of this proof_wanted has already been satisfied.