= Solution
Since $A$ is a <regular local ring>, $\dim A=d$ is finite. Choose a chain of <prime ideals> of length $d$,
$$
\mathfrak p_0\subsetneq\mathfrak p_1\subsetneq\cdots\subsetneq\mathfrak p_d=\mathfrak m.
$$
Such a chain exists because the supremum defining this finite integer <Krull dimension> is attained; a maximal-length chain in a <local ring> ends at its <maximal ideal>.
For each $i$, the <ideal> $\mathfrak p_i$ is finitely generated because $A$ is <Noetherian>. This ensures that its extension $\mathfrak p_iB$ consists precisely of series all of whose coefficients lie in $\mathfrak p_i$: if $\mathfrak p_i=(b_1,\ldots,b_r)$, write each coefficient as $\sum_j b_jc_{jn}$ and gather them into the finitely many series $\sum_n c_{jn}x^n$. Thus coefficient reduction gives
$$
B/\mathfrak p_iB\cong(A/\mathfrak p_i)[[x]].
$$
The coefficient ring $A/\mathfrak p_i$ is an <integral domain>, and so is its <formal power series ring>: the first nonzero coefficient of a product is the product of the first nonzero coefficients of its factors. Hence each $\mathfrak p_iB$ is prime. Also $\mathfrak p_iB\cap A=\mathfrak p_i$, so the strict inclusions persist upon extension. Finally, $x\notin\mathfrak mB$, since its image in $B/\mathfrak mB\cong k[[x]]$ is nonzero. We obtain the prime chain
$$
\mathfrak p_0B\subsetneq\cdots\subsetneq\mathfrak p_dB=\mathfrak mB\subsetneq\mathfrak mB+(x)=I
$$
of length $d+1$. Therefore $\dim B\geq d+1$. Together with part (b),
$$
\boxed{\dim A[[x]]=d+1.}
$$
Its <embedding dimension> is also $d+1$, by part (b), so $B$ is itself a <regular local ring>. This proves that <formal power series preserve regular local rings>.
Back to article page
