Solution (source code)

= Solution

A <ring extension> $A\subseteq B$ is <module-finite ring extension>[finite] when $B$ is a <finitely generated module> over $A$. Every finite extension is integral by the <determinant trick>.