[Merged by Bors] - feat (RingTheory/PowerSeries): Add basic lemmas aiming at proving that power series over a field are a DVR

[faenuccio]

Add some basic lemmas about (univariate) power series over fields and their inverses, aiming at proving that they form a DVR.

Co-authored-by: María Inés de Frutos Fernández @mariainesdff

[riccardobrasca]

bors d+

[mathlib-bors]

✌️ faenuccio can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[faenuccio]

@riccardobrasca I have done several additions/modifications, you might want to have another round of reviews before I merge. In particular, I am shocked on how this line could possibly work (and solve all decidability issues).

[riccardobrasca]

@riccardobrasca I have done several additions/modifications, you might want to have another round of reviews before I merge. In particular, I am shocked on how this line could possibly work (and solve all decidability issues).

I think this is more or less the same as opening Classical. I don't know if it is possible to have a "true" (I mean not given by choice, but by an actual algorithm) decidable equality on power series in certain cases, but if it is that line will probably create diamonds.

[faenuccio]

@riccardobrasca I have done several additions/modifications, you might want to have another round of reviews before I merge. In particular, I am shocked on how this line could possibly work (and solve all decidability issues).

I think this is more or less the same as opening Classical. I don't know if it is possible to have a "true" (I mean not given by choice, but by an actual algorithm) decidable equality on power series in certain cases, but if it is that line will probably create diamonds.

So what do you suggest me to do? To leave as it is, to open Classical or to manually add [Decidable (f =0)] (and [Decidable (0=0)] on one occasion) all the time?

[riccardobrasca]

@riccardobrasca I have done several additions/modifications, you might want to have another round of reviews before I merge. In particular, I am shocked on how this line could possibly work (and solve all decidability issues).

I think this is more or less the same as opening Classical. I don't know if it is possible to have a "true" (I mean not given by choice, but by an actual algorithm) decidable equality on power series in certain cases, but if it is that line will probably create diamonds.

So what do you suggest me to do? To leave as it is, to open Classical or to manually add [Decidable (f =0)] (and [Decidable (0=0)] on one occasion) all the time?

Thinking more about it, it seems impossible to have an actual algorithm to decide equality, so opening Classical should be fine. Sorry for the noise.

[faenuccio]

@riccardobrasca I have done several additions/modifications, you might want to have another round of reviews before I merge. In particular, I am shocked on how this line could possibly work (and solve all decidability issues).

I think this is more or less the same as opening Classical. I don't know if it is possible to have a "true" (I mean not given by choice, but by an actual algorithm) decidable equality on power series in certain cases, but if it is that line will probably create diamonds.

So what do you suggest me to do? To leave as it is, to open Classical or to manually add [Decidable (f =0)] (and [Decidable (0=0)] on one occasion) all the time?

Thinking more about it, it seems impossible to have an actual algorithm to decide equality, so opening Classical should be fine. Sorry for the noise.

Done! And thanks for all your comments.

[riccardobrasca]

Thanks!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style