Formal expansion at a smooth point (source code)

= Formal expansion at a smooth point
{title2=$\widehat{\mathcal O}_{X,x}\cong k[[T_1,\ldots,T_d]]$}

A chosen <regular system of parameters> gives the displayed completion isomorphism by sending $T_i$ to $t_i$. The <associated graded ring of a regular local ring> is the polynomial ring on their initial forms. Successively removing the homogeneous initial form of each remainder gives a unique formal series for every local function. The <Krull intersection theorem> embeds the local ring in its completion. The power-series characterization is also given in https://stacks.math.columbia.edu/tag/0C0S[Stacks Project Lemma 10.160.10].