Stream: maths

Lambert A'Campo (Jan 05 2021 at 20:40):

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 (Jan 05 2021 at 20:53):

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

Johan Commelin (Jan 05 2021 at 20:54):

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 (Jan 05 2021 at 20:55):

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 (Jan 05 2021 at 20:55):

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

Lambert A'Campo (Jan 05 2021 at 21:46):

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

Last updated: May 11 2021 at 16:22 UTC