Commit 2024-07-05 11:29 c6553164

View on Github →

feat: add properties of the X-adic valuation on PowerSeries K (#13064) Add some properties of the $X$-adic valuation on the rings $K[X]$ and $K[[X]]$ when $K$ is a field. It is an intermediate step towards the proof that the $X$-adic completion of $K(X)$ is isomorphic to $K((X))$.

Estimated changes