Commit 2025-09-22 13:29 76eb9c0c
View on Github →feat: restricted power series form a ring (#26089) We define restricted power series over a normed ring R, and show they form a ring when R has the ultrametric property <NEWLINE> This is an update of [#23338](https://github.com/leanprover-community/mathlib4/pull/23338) to meet new expectations of PRs from forks.