@TimCampion Since I did not want to digress too much from the topic of your answer, I have added some stuff related to our recent discussion in comment in the MathOverflow chatroom.
I apologize for posting here something unrelated to homotopy theory - but this was the only room I was able to find where Tim Campion was pingable.
Given a spectrum X, I can form Sym(X), the free E_oo-ring spectrum on X, which is somewhat analogous to the polynomial ring in one variable X. It seems to me that there should also be an analog of the formal power series ring in one variable. For example, the underlying spectrum of Sym(X) is the sum of D_n(X), whereas I would expect this to be the product for the formal power series version. Has this been written about somewhere?
