JetBrains / arend-lib

Apache License 2.0
79 stars 23 forks source link

Prove that the radical of the ideal generated by two elements is equal to the radical of the ideal generated by powers of these elements #41

Closed valis closed 2 years ago

valis commented 2 years ago

This is AG.Scheme/pow-lin-comb. Explicitly, this just means that if e^k = a*c + b*d, then there are t, s, and l such that e^l = t*a^n + s*b^m.

TurtlePU commented 2 years ago

I'll take it; I am not going to provide a generalization for now, though.