[proofplan] We apply the [Bass-Heller-Swan decomposition](/theorems/8686) to the Laurent [polynomial ring](/page/Polynomial%20Ring) $R[t,t^{-1}]$. That decomposition expresses $K_1(R[t,t^{-1}])$ as the direct sum of $K_1(R)$, $K_0(R)$, and two copies of the nil group $NK_1(R)$. Since $R$ is regular Noetherian, the nil group $NK_1(R)$ vanishes. Removing the two zero summands gives the desired decomposition. [/proofplan]

[step:Apply the Bass-Heller-Swan decomposition to $R$]Let $L$ denote the Laurent polynomial ring $R[t,t^{-1}]$. Since $R$ is a unital ring, the Bass-Heller-Swan decomposition applies to $R$. By [citetheorem:8675], there is a natural decomposition of abelian groups \begin{align*} K_1(L)\cong K_1(R)\oplus K_0(R)\oplus NK_1(R)\oplus NK_1(R). \end{align*} Here $NK_1(R)$ denotes the Bass nil group measuring the kernel of the evaluation-induced map from polynomial $K_1$ back to $K_1(R)$.[/step]

[guided]We first isolate the structural input. Define \begin{align*} L:=R[t,t^{-1}]. \end{align*} The theorem [citetheorem:8675] applies to every unital ring. The present ring $R$ is commutative and unital by hypothesis, so in particular it is a unital ring, and the hypotheses of Bass-Heller-Swan are satisfied. Therefore it gives an isomorphism of abelian groups \begin{align*} K_1(R[t,t^{-1}])\cong K_1(R)\oplus K_0(R)\oplus NK_1(R)\oplus NK_1(R). \end{align*} The first summand is induced by viewing matrices over $R$ as constant matrices over $R[t,t^{-1}]$. The second summand is the Bass suspension, or Laurent-parameter, summand. The remaining two summands are the nil summands $NK_1(R)$, which record the possible failure of polynomial homotopy invariance in degree $1$.[/guided]

[step:Use regularity to make the nil summands vanish] Because $R$ is a regular Noetherian commutative ring, [citetheorem:8674] gives \begin{align*} NK_1(R)=0. \end{align*} Substituting this into the Bass-Heller-Swan decomposition gives \begin{align*} K_1(R[t,t^{-1}])\cong K_1(R)\oplus K_0(R)\oplus 0\oplus 0. \end{align*} [/step]

[step:Remove the zero direct summands] For every abelian group $A$, the canonical maps $A\oplus 0\to A$ and $A\to A\oplus 0$ are inverse isomorphisms. Applying this twice to \begin{align*} K_1(R)\oplus K_0(R)\oplus 0\oplus 0 \end{align*} yields an isomorphism \begin{align*} K_1(R)\oplus K_0(R)\oplus 0\oplus 0 \cong K_1(R)\oplus K_0(R). \end{align*} Composing this isomorphism with the Bass-Heller-Swan isomorphism after the vanishing of $NK_1(R)$ gives \begin{align*} K_1(R[t,t^{-1}])\cong K_1(R)\oplus K_0(R). \end{align*} This is the asserted decomposition. [/step]