Lemma 15.48.3. Let $(R, \mathfrak m, \kappa )$ be a regular local ring. Let $m \geq 1$. Let $f_1, \ldots , f_ m \in \mathfrak m$. Assume there exist derivations $D_1, \ldots , D_ m : R \to R$ such that $\det _{1 \leq i, j \leq m}(D_ i(f_ j))$ is a unit of $R$. Then $R/(f_1, \ldots , f_ m)$ is regular and $f_1, \ldots , f_ m$ is a regular sequence.

Proof. It suffices to prove that $f_1, \ldots , f_ m$ are $\kappa$-linearly independent in $\mathfrak m/\mathfrak m^2$, see Algebra, Lemma 10.106.3. However, if there is a nontrivial linear relation the we get $\sum a_ i f_ i \in \mathfrak m^2$ for some $a_ i \in R$ but not all $a_ i \in \mathfrak m$. Observe that $D_ i(\mathfrak m^2) \subset \mathfrak m$ and $D_ i(a_ j f_ j) \equiv a_ j D_ i(f_ j) \bmod \mathfrak m$ by the Leibniz rule for derivations. Hence this would imply

$\sum a_ j D_ i(f_ j) \in \mathfrak m$

which would contradict the assumption on the determinant. $\square$

In your comment you can use Markdown and LaTeX style mathematics (enclose it like $\pi$). A preview option is available if you wish to see how it works out (just click on the eye in the toolbar).