Radical in Noetherian Ring

Stream: maths

[Lambert A'Campo]

Let R be a Noetherian ring and I an ideal of R, then there exists an integer n such that rad(I)^n is contained in I. A common proof is to choose generators x_1, ..., x_k of I and integers m_i such that x_i^(m_i) in A, now n = 1 + sum (m_i - 1) works 'by binomial expansion'. What is a better proof that can be put in lean?

[Johan Commelin]

I haven't thought this through, but would induction on the number of generators make things easier?

[Johan Commelin]

So, I imagine that you'll get some s : finset R, and I = ideal.span s. And now you could try finset.induction_on s.

[Johan Commelin]

Then you have to prove things for ideal.span (insert r s), under the assumption that your claim is true for ideal.span s.

[Johan Commelin]

It seems like you can then use the "binary" binomial formula, which looks easier to use in practice.

[Lambert A'Campo]

That sounds about right. I guess some dirty computations can't be avoided.