On formal solutions to differential equations Let $k$ be a field of characteristic zero. Put $K=k[\![ t]\!]$ and $W=k\langle t,\partial\rangle / ([\partial,t]=1)$. Then $W$ operates on $K$ in the obvious way ($\partial f = \frac{d f}{dt}$), and define 
$$
  K^\text{fin} = \{f\in K:D f=0\text{ for some }D\in W\smallsetminus 0\} .
$$
The question is: 

Is $K^\text{fin}$ a subring of $K$?

Apologies in advance if this question is too elementary. Assuming $K^\text{fin}$ is a ring, I would be interested if anyone knows of somewhere in which arises naturally. 
 A: These are (more or less) called holonomic functions. They appear in combinatorics as the generating functions of a large class of sequences (those satisfying linear recurrences with polynomial coefficients), and they're known to be closed under addition and multiplication. Here is a proof which is due to Stanley although the result is some decades older:
For $f \in k((t))$ let $L_f$ denote the $k(t)$-span of $\{ f, f', f'', ..., \}$ in $k((t))$. Then $f$ is holonomic iff $L_f$ is finite-dimensional. Since $L_{f+g} \subseteq L_f + L_g$ and $L_{fg} \subseteq L_f L_g$ it follows that if $L_f$ and $L_g$ are both finite-dimensional then so are $L_{f+g}$ and $L_{fg}$. Moreover $\dim L_{f+g} \le \dim L_f + \dim L_g$ and $\dim L_{fg} \le \dim L_f \dim L_g$. 
A: Your $K^\mathrm{fin}$ is certainly closed under linear combinations with coefficients in $k$. In particular if $D_1 f_1 = 0$ and $D_2 f_2 = 0$, then the pair $(f,f_2) = (f_1+f_2,f_2)$ ($f$ could also be a different linear combination) will satisfy the system of equations $D_1 f = D_1 f_2$, $D_2 f_2 = 0$. Now, it remains to differentiate the first equation as many times as needed to eliminate $f_2$ and its derivatives. After elimination you'll have an equation $Df = 0$ in terms of $f$ and its derivatives alone. To make sure that you need to differentiate only finitely many times, every time a derivative of $f_2$ of order equal to or greater than the order of $D_2$, it can be eliminated using the equation $D_2 f_2 = 0$. So, the number of times you need to differentiate $D_1 f = D_1 f_2$ to eliminate $f_2$ is bounded by the order of $D_2$. This is a classic trick, though I don't know whether it has any name or standard reference associated to it.
Of course, you can play the same game with $(f,f_2) = (f_1 f_2,f_2)$ and the system of equations $D_1(f/f_2) = 0$, $D_2 f_2 = 0$. However, after eliminating $f_2$ and its derivatives in the naive way, you end up with a non-linear equation for $f$. It is not clear to me at the moment whether differentiating a larger number of times than one might naively expect could result in a linear equation for $f$. So I don't know the answer to the question of the closure of $K^\mathrm{fin}$ under multiplication. I've also not found a counter example.
A: I don't know the answer in this generality, but the following paper may be relevant:
MR0320402
Frank, Günter; Wittich, Hans
Zur Theorie linearer Differentialgleichungen im Komplexen. 
Math. Z. 130 (1973), 363–370. 
In this paper the question is studied when $k$ is the field of complex numbers, and
the set of differential operators is somewhat restricted.
