Rank inequality for an injection of finite free modules (source code)

= Rank inequality for an injection of finite free modules

Over a nonzero commutative ring, an injection $R^m\hookrightarrow R^n$ implies $m\leq n$. If $m>n$, appending zero coordinates gives an injective endomorphism of $R^m$ with zero determinant; the Cayley--Hamilton theorem and cancellation of that injection eventually force the identity to vanish.