I've always been a bit annoyed by expressions like $$\sum_{n:\mathbb{N}} a_n$$ when the relevant limit doesn't converge, for the following reason: if you're not going to tell the reader what ring this entity lives in and/or what it means for two such expressions to be equal, then why bother writing it? Anyway, I had an idea for formalizing the meaning of such expressions. Write $\mathbb{R}[[x]]$ for the ring of formal power series in one variable $x$. Given $x_0 \in \mathbb{R}$ and $p \in \mathbb{R}[[x]]$, write $[x_0/x]p$ for the result of substituting $x_0$ for $x$ in $p$. Now call $p \in \mathbb{R}[[x]]$ strongly vanishing iff $[1/x]p$ exists and equals $0$. I can't quite tell whether or not this is an ideal, so lets compensate by defining that $p$ is weakly vanishing iff it is an element of the ideal generated by the strongly vanishing elements. Write $I$ for the ideal of weakly vanishing elements of $R[[x]]$. We can then define that a formal series is an element of the quotient ring $R[[x]]/I$. The idea is to reinterpret $$\sum_{n:\mathbb{N}} a_n,$$ as being the formal series that corresponds to the formal power series $$\sum_{n:\mathbb{N}} a_n x^n.$$
Question. Is the step in which we pass to the ideal generated by the strongly vanishing elements actually necessary?
That is, do the strongly vanishing elements of $R[[x]]$ form an ideal?
The strongly vanishing elements do not form an ideal. For a very simple counterexample, $1-x$ is strongly vanishing, but $(1-x)\sum x^n=1$ is not. This example shows that in fact the ideal they generate is all of $\mathbb{R}[[x]]$.
More generally, let $p(x)=\sum a_nx^n$ be any strongly vanishing series such that $a_0\neq0$. Given another formal power series $q(x)=\sum b_nx^n$, let $s_N$ be the sum of the first $N$ terms of $p(x)q(x)$ evaluated at $x=1$. Note that we can write $s_N=a_0b_N+c$, where $c$ only depends on $b_0,\dots,b_{N-1}$. Therefore we can easily inductively construct a sequence $(b_n)$ such that the partial sums $s_N$ form any sequence at all. (In particular, choosing the partial sums to all be $1$ shows that $p(x)$ is a unit, and so in fact every power series is a multiple of $p(x)$!)