Solution (source code)

= Solution

Let $S=R[\phi]$ be the commutative subring of <endomorphisms> generated by scalar multiplication and $\phi$. Commutativity follows because the scalar maps commute with the $R$-linear map $\phi$, and every element of $S$ is a polynomial in $\phi$ with scalar coefficients. Thus <determinants> and the <adjugate identity> apply to matrices over $S$.

With the convention for the coefficients in the question, the column of generators satisfies
$$
C\begin{pmatrix}m_1\\\vdots\\m_n\end{pmatrix}=0,\qquad C=(a_{ij}-\phi\delta_{ij}).
$$
Multiply by $\operatorname{adj}(C)$ over $S$. Since $\operatorname{adj}(C)C=(\det C)I_n$, the endomorphism $\det C$ kills every generator $m_i$. It therefore kills every element $\sum r_i m_i$ of the <module>, by $R$-linearity. Hence it is the zero endomorphism, and
$$
\boxed{\det(a_{ij}-\phi\delta_{ij})=0\quad\text{in }R[\phi].}
$$
The argument does not require the generating set to be a <basis>; relations among the generators cause no difficulty. This is the <determinant trick>.