Hilbert basis theorem

Stream: Is there code for X?

[Riccardo Brasca]

Are we really missing Hilbert basis theorem for power series? We have docs#PowerSeries.isNoetherianRing, but not the version over a noetherian ring I think.

[Riccardo Brasca]

randomly tagging @Filippo A. E. Nuccio and @Antoine Chambert-Loir that are working on power series

[Riccardo Brasca]

@loogle "powerseries", "noetherian"

[loogle]

:search: PowerSeries.isNoetherianRing

[Filippo A. E. Nuccio]

We indeed have very little for power series over arbitrary base rings, but this calls for some improvement! I cannot commit to work on this immediately, but I'm happy to put this in my ToDo list (aka: things I'll never do :shrug: )

[Riccardo Brasca]

no no, I will put it on the TODO list of some students!

[Christian Merten]

I think more generally showing that the adic completion of a noetherian ring is noetherian would be a nice project.

[Ruben Van de Velde]

Do we have a place for "nice projects"? GitHub issues? :innocent:

[Johan Commelin]

We already have github issues with good-first-issue. I guess we can also have ones that are labeled nice :stuck_out_tongue_wink:

[Riccardo Brasca]

In this case one bound the number of generators of the ideal in terms of the number of generators in the ring (via P ↦ P(0) ), and I need this more precise result to show that power series over a PID are a UFD.