symmetric monoidal (∞,1)-category of spectra
A power series in a variable $X$ and with coefficients in a ring $R$ is a series of the form
where $a_n$ is in $R$ for each $n\ge 0$. Given that there are no additional convergence conditions, a power series is also termed emphatically as a formal power series. If $R$ is commutative, then the collection of formal power series in a variable $X$ with coefficients in $R$ forms a commutative ring denoted by $R [ [ X ] ]$.
More generally, a power series in $k$ commuting variables $X_1,\ldots, X_k$ with coefficients in a ring $R$ has the form $\sum_{n_1=0,n_2=0,\ldots, n_k = 0}^\infty a_{n_1\ldots n_k} X_1^{n_1} X_2^{n_2}\cdots X_k^{n_k}$. If $R$ is commutative, then the collection of formal power series in $k$ commuting variables $X_1,\ldots, X_k$ form a formal power series ring denoted by $R [ [ X_1,\ldots, X_k ] ]$.
More generally, we can consider noncommutative (associative unital) ring $R$ and words in noncommutative variables $X_1,\ldots, X_k$ of the form
(where $m$ has nothing to do with $k$) and with coefficient $a_w \in R$ (here $w$ is a word of any length, not a multiindex in the previous sense). Thus the power sum is of the form $\sum_w a_w X_w$ and they form a formal power series ring in variables $X_1,\ldots, X_k$ denoted by $R\langle \langle X_1,\ldots, X_k \rangle\rangle$. Furthermore, $R$ can be even a noncommutative semiring in which case the words belong to the free monoid on the set $S = \{ X_1,\ldots, X_k\}$, the partial sums are then belong to a monoid semiring $R\langle S\rangle$. The formal power series then also form a semiring, by the multiplication rule
Of course, this implies that in a specialization, $b$-s commute with variables $X_{i_k}$; what is usually generalized to take some endomorphisms into an account (like at noncommutative polynomial level of partial sums where we get skew-polynomial rings, i.e. iterated Ore extensions).
For a natural number $k$, a power series $\sum_{n=0}^\infty a_n X^n$ such that $a_n = 0$ for all $n \gt k$ is a polynomial of degree at most $k$.
For $f \in C^\infty(\mathbb{R})$ a smooth function on the real line, and for $f^{(n)} \in C^\infty(\mathbb{R})$ denoting its $n$th derivative its MacLaurin series (its Taylor series at $0$) is the power series
If this power series converges to $f$, then we say that $f$ is analytic.
This follows easily from the observation that we can invert $1 + x b$ for any power series $b$ by forming $1 - x b + x^2 b^2 - \ldots$ and collecting only finitely many terms in each degree. As a simple corollary,
$R[ [x_1, \ldots, x_n] ]$ equipped with the ideal $(x_1, \ldots, x_n)$ is the free adic $R$-algebra on $n$ generators, in the sense that it is the value of the left adjoint $Pow$ to the forgetful functor
as applied to the set $\{x_1, \ldots, x_n\}$.
The idea is that for each adic $R$-algebra $(S, I)$ and element $(s_1, \ldots s_n) \in I^n$, there is a unique adic algebra map $R[ [x_1, \ldots, x_n] ] \to S$ that sends $x_i$ to $s_i$; this adic algebra map sends a power series $\sum a_{k_1, \ldots, k_n} x_1^{k_1} x_n^{k_n}$ to the sequence of truncations
belonging to $\underset{\longleftarrow}{\lim}_k S/I^k \cong S$.
It follows that we may define a clone or cartesian operad as follows: the $n^{th}$ component is the set $I_n = (x_1, \ldots, x_n) \subset R[ [x_1, \ldots, x_n] ]$ which is the monad value $Ideal Pow(\{x_1, \ldots, x_n\})$. Letting $M$ denote the monad $Ideal \circ Pow$, with monad multiplication $\mu$, and $[n]$ the set $\{x_1, \ldots, x_n\}$, the clone multiplication
is the composition of the maps
The clone multiplication thus defined is called substitution of power series; it takes a tuple consisting of $p(x_1, \ldots, x_n) \in I_n, q_1(x_1, \ldots x_k) \in I_k, \ldots q_n(x_1, \ldots, x_k) \in I_k)$ to a power series denoted as
The resulting clone or operad yields, in the particular case $k = n = 1$, an associative substitution operation
with $sub(p, q) = p \circ q$ the power series $p(q(x))$.
The group of invertible elements in the substitution monoid $x R[ [x] ]$ consists of power series of the form $a_1 x + a_2 x^2 + \ldots$ where $a_1$ is multiplicatively invertible in the ring $R$.
In other words, we can functionally invert a power series provided that the linear coefficient $a_1$ is invertible in $R$.
Given power series $a = a_1 x + a_2 x^2 + \ldots$ and $b = b_1 x + b_2 x^2 + \ldots$, we may read off coefficients of the composite $a \circ b$ as
where in particular $(a \circ b)_1 = a_1 b_1$. Now $a$ is the left functional inverse of $b$, or $b$ is the right inverse of $a$, if $(a \circ b)(x) = x$, i.e., if $(a \circ b)_k = 1$ if $k = 1$ and $0$ otherwise. The first equation says simply $(a \circ b)_1 = a_1 b_1 = 1$ which implies $a_1$ is invertible. Conversely, if $a_1$ is multiplicatively invertible and $b_1 = a_1^{-1}$, then the equations
may be uniquely solved for the remaining $a_i$'s given the $b_j$'s, and uniquely solved for the remaining $b_j$'s given the $a_i$'s, by an inductive procedure: for $k \neq 1$ we have
and this allows us to solve for $b_k$,
given the values $a_1, \ldots, a_k$ and earlier $b$-values $b_{k_j}$ for $k_j \lt k$ given by inductive hypothesis. Similarly we can solve for $a_k$ in terms of given coefficients $b_1, \ldots, b_k$ and earlier $a$-values $a_n$, $n \lt k$. Thus every power series $a$ has a right inverse if $a_1^{-1}$ exists, and $b$ has a left inverse if $b_1^{-1}$ exists, and this completes the proof.
A formalization in homotopy type theory and there in Coq is discussed in section 4 of
The discussion of the differentiation of a converging power series term by term is at