[proofplan] We prove invariant basis number by reducing an isomorphism of finite free $R$-modules to an isomorphism of finite-dimensional vector spaces. Since $R$ is nonzero, it has a maximal ideal $\mathfrak m$, and the residue ring $k=R/\mathfrak m$ is a field. Tensoring an assumed isomorphism $R^m\cong R^n$ with $k$ over $R$ gives an isomorphism $k^m\cong k^n$, and invariance of vector-space dimension then forces $m=n$. [/proofplan]

[step:Choose a residue field of the nonzero ring] Let $R$ be a nonzero commutative unital ring. By the standard maximal ideal theorem for nonzero commutative unital rings, there exists a maximal ideal $\mathfrak m\trianglelefteq R$. Define the [quotient ring](/page/Quotient%20Ring) \begin{align*} k := R/\mathfrak m. \end{align*} Since $\mathfrak m$ is maximal, the standard quotient criterion for maximal ideals implies that $k$ is a field. Let \begin{align*} \pi:R\to k \end{align*} be the quotient homomorphism. We regard $k$ as a left $R$-module through $\pi$, so that $r\cdot a=\pi(r)a$ for $r\in R$ and $a\in k$. [/step]

[step:Tensor an arbitrary free-module isomorphism with the residue field]Let $m,n\geq 0$ be integers, and suppose that \begin{align*} \Phi:R^m\to R^n \end{align*} is an isomorphism of left $R$-modules. Define the induced map \begin{align*} \operatorname{id}_k\otimes_R \Phi:k\otimes_R R^m\to k\otimes_R R^n \end{align*} by \begin{align*} a\otimes x\mapsto a\otimes \Phi(x). \end{align*} This map is an isomorphism, with inverse $\operatorname{id}_k\otimes_R \Phi^{-1}$, because [tensor product](/page/Tensor%20Product) over $R$ is functorial and preserves inverse pairs of maps.[/step]

[guided]We start with the precise object whose rank we want to test. Let $m,n\geq 0$ be integers, and assume that \begin{align*} \Phi:R^m\to R^n \end{align*} is an isomorphism of left $R$-modules. To compare $m$ and $n$, we pass from modules over $R$ to vector spaces over the field $k=R/\mathfrak m$. The passage is made by tensoring over $R$ with the left $R$-module $k$. Define \begin{align*} \operatorname{id}_k\otimes_R \Phi:k\otimes_R R^m\to k\otimes_R R^n \end{align*} on pure tensors by \begin{align*} a\otimes x\mapsto a\otimes \Phi(x). \end{align*} This formula is well-defined by the [universal property of the tensor product](/theorems/3971), since the assignment $(a,x)\mapsto a\otimes \Phi(x)$ is $R$-balanced. Now we verify that the induced map is an isomorphism rather than merely a homomorphism. Since $\Phi$ is an isomorphism, it has an $R$-linear inverse \begin{align*} \Phi^{-1}:R^n\to R^m. \end{align*} Functoriality of tensor product gives maps $\operatorname{id}_k\otimes_R\Phi$ and $\operatorname{id}_k\otimes_R\Phi^{-1}$. Their composites are \begin{align*} (\operatorname{id}_k\otimes_R\Phi^{-1})\circ(\operatorname{id}_k\otimes_R\Phi) = \operatorname{id}_k\otimes_R(\Phi^{-1}\circ\Phi) = \operatorname{id}_k\otimes_R\operatorname{id}_{R^m} = \operatorname{id}_{k\otimes_R R^m}. \end{align*} Similarly, \begin{align*} (\operatorname{id}_k\otimes_R\Phi)\circ(\operatorname{id}_k\otimes_R\Phi^{-1}) = \operatorname{id}_{k\otimes_R R^n}. \end{align*} Therefore $\operatorname{id}_k\otimes_R\Phi$ is an isomorphism with inverse $\operatorname{id}_k\otimes_R\Phi^{-1}$.[/guided]

[step:Identify the tensor products with finite-dimensional vector spaces] For every integer $q\geq 0$, define the $k$-[linear map](/page/Linear%20Map) \begin{align*} \Theta_q:k\otimes_R R^q\to k^q \end{align*} by \begin{align*} a\otimes (r_1,\dots,r_q)\mapsto (a\pi(r_1),\dots,a\pi(r_q)). \end{align*} This is the standard base-change isomorphism for finite free modules, with inverse sending the $i$-th standard basis vector of $k^q$ to $1_k\otimes e_i$, where $e_i$ is the $i$-th standard basis vector of $R^q$. Hence \begin{align*} k\otimes_R R^m\cong k^m \end{align*} and \begin{align*} k\otimes_R R^n\cong k^n. \end{align*} Combining these identifications with $\operatorname{id}_k\otimes_R\Phi$, we obtain an isomorphism of $k$-vector spaces \begin{align*} k^m\cong k^n. \end{align*} [/step]

[step:Compare vector-space dimensions to recover the ranks] Since $k$ is a field, $k^m$ and $k^n$ are finite-dimensional vector spaces over $k$. Their dimensions are \begin{align*} \dim_k(k^m)=m \end{align*} and \begin{align*} \dim_k(k^n)=n. \end{align*} Isomorphic finite-dimensional vector spaces over a field have the same dimension, so the isomorphism $k^m\cong k^n$ gives \begin{align*} m=n. \end{align*} Thus every isomorphism $R^m\cong R^n$ of finite free left $R$-modules has $m=n$, and therefore $R$ has invariant basis number. [/step]