regular system of parameters equivalent basis

Given: The objects and hypotheses in the statement. We work with the Axiom of Choice; cited dependent-choice and resolution-existence hypotheses are retained.

regular system of parameters: In a regular local ring $(R,\mathfrak{m},k)$ of dimension $d$, an ordered minimal generating tuple $(x_1,\dots ,x_d)$ of $\mathfrak{m}$ is a regular system of parameters. The tuple is empty when $d=0$. This definition concerns generators of the maximal ideal; the regular-sequence property is a theorem, not part of the definition.

embedding dimension is minimal maximal ideal generator number: Under the Choice assumption used in its proof, for a nonzero Noetherian local ring $(R,\mathfrak{m},k)$, $\mathrm{edim}R$ is the least number of generators of $\mathfrak{m}$.

Assuming the Axiom of Choice, generators modulo an ideal in the Jacobson radical lift to generators: Assume the Axiom of Choice. Let $R$ be a commutative ring, let $I⊴R$ satisfy $I\subseteq J(R)$, and let $M$ be a finitely generated left $R$-module. If elements $x_1,\dots ,x_r\in M$ generate $M\mathrm{/}IM$, then $x_1,\dots ,x_r$ generate $M$.