Let $\mathbb{k}$ be a field (we can suppose $k=\mathbb{R}$ or $\mathbb{C}$ if necessary). Let $M_n(\mathbb{k})$ denote the ring of matrices with entries in $\mathbb k$.
Recall that a ring $R$ has the invariant basis number (IBN) property if any two bases of a finitely generated free $R$-module must have the same cardinality.
Question: Does $M_n(\mathbb{k})$ have the invariant basis number property?
I've been able to find a result saying that any commutative $R$ has IBN. On the other hand, the simplest $R$ that I came across without IBN, namely the column finite matrices, involves infinite indexing sets. This would suggest that $M_n(\mathbb{k})$ has IBN, but I don't have a proof/reference for this fact.
Best Answer
Let us say that a matrix $M\in M_{p\times q}(R)$ is invertible if there exists $N\in M_{q\times p}(R)$ such that $MN=I_p$ and $NM=I_q$.
Lemma. A ring $R$ has IBN if and only if an invertible matrix with entries in $R$ is a square matrix.
Assuming the lemma, which is well-known (and easy to prove), you can see that $M_n(k)$ has IBN, since we have a canonical identification $M_{p\times q}(M_n(k))\simeq M_{pn\times qn}(k)$ sending invertible matrices to invertible matrices.
In fact, the same argument shows:
Thm. If $R$ has IBN, so has $M_n(R)$ for all $n\geq 1$.
Another way to prove what you want is to use the following known theorem, since $M_n(k)$ is left noetherian:
Thm. Assume that for all $m\geq 1$, any surjective $R$-linear map $u:R^m\to R^m$ is bijective. Then $R$ has IBN. In particular, any left (or right) noetherian ring has IBN.
Proof. Let us prove the first part. It is enough to prove that $R^n\simeq_R R^m\Rightarrow n=m$, for all $n,m\geq 1$.
Let $u:R^m\overset{\sim}{\to} R^n$ be an $R$-module isomorphism. One may assume that $m\geq n$. Composing with projection onthe first components $\pi:R^m\to R^n$, we get a surjective linear map $\pi\circ u:R^m\to R^m$, which is bijective by assumption. Since $u$ is bijective, $\pi$ is bijective, which forces $n=m$.
The second part comes from the well-known fact that if $R$ is noetherian , any surjective $R$-linear map $R^m\to R^m$ is bijective (consider the chain $\ker(u^n)\subset \ker(u^{n+1})$ for all $n\geq 1$)