Proving that every basis of $R^n$ has $n$ elements I've been studying modules and I found a statement that isn't quite clear to me. The statement goes as follows,

When there exists a surjective ring homomorphism $R\rightarrow K$, with $K$ a field, then every basis of $R^n$ has $n$ elements.

Can anybody help me understand why this is the case?
 A: I don't even think one even needs the morphism to be surjective (at least, provided your definition of ring homomorphism includes taking $1$ to $1$). And in fact, $K$ does not need to be a field; any ring satisfying the invariant basis property will suffice. As I recall, one has the following argument, which I first learned from T.Y. Lam's "Lectures on Modules and Rings":
Suppose $m$ is a positive integer such that $R^{n}$ admits a basis with $m$ elements. This is tantamount to providing an isomorphism of $R$-modules $\varphi \colon R^{m} \to R^{n}$. Indeed, suppose $r_{1}, \ldots, r_{m} \in R^{n}$ are your basis elements. The (unique) morphism of $R$-modules $R^{m} \to R^{n}$ sending the $i$th standard idempotent $e_{i}$ to $r_{i}$ must be surjective, since the $r_{i}$s generate $R^{n}$. On the other hand, this morphism must also be injective, since there are no nontrivial $R$-linear relations between the $r_{i}$s.
The data of $\varphi$, in turn, is the same as supplying matrices $A, B$ with entries in $R$ of the correct dimensions such that $AB = I_{m}, BA = I_{n}$. Applying the morphism $R \to K$ entrywise to $A, B$, we obtain matrices $A', B'$ with entries in $K$ such that $A'B' = I_{m}, B'A' = I_{n}$. But these matrices then define $K$-linear maps $K^{m} \to K^{n}, K^{n} \to K^{m}$ which are inverse to each other, and so we must have $n = m$ by usual linear algebra (or the invariant basis property).
(Alternatively, you can use the functor $M \mapsto M \otimes_{R} K$ from $R$-modules to $K$-modules given by extension of scalars, and by functoriality one sees that $\varphi \otimes_{R} \mathrm{Id}_{K} \colon K^{m} \to K^{n}$ must be an isomorphism. In the non-commutative setting, you need to pay a little attention to the "sidedness" of the modules under consideration, but this argument indeed goes through fine.)
