Corollary 4

Let $A$ be a regular ring and $P$ a finitely generated projective $A$-module. The symmetric algebra $S_A(P)$ is a regular ring.

Let $p$ be a prime ideal of $S_A(P)$ and $q$ its inverse image in $A$. The local ring $S_A(P)_p$ is a ring of fractions of the ring $S_A(P)_q$, which is isomorphic to $S_{A_q}(P_q)$ (A, III, p. 72, prop. 7); it is enough to prove that the latter is regular. This reduces us to the case where $A$ is local; but then $P$ is free of finite type. By prop. 1 of No. 1 and A, X, p. 143, cor. 1, one has $dh(S_A(P)) = dh(A) + rg_A(P) < +\infty$, and $S_A(P)$ is regular by prop. 4.