It's common to use the axiom of choice to prove that nonzero commutative rings have the invariant basis number property: in other words, that for a nonzero commutative ring $ R $, the $ R $-modules $ R^m $ and $ R^n $ are isomorphic if and only if $ m = n $.

The most common proof of this uses Zorn's lemma to find a maximal ideal $ \mathfrak m $ of $ R $. We can then tensor any isomorphism $ R^m \to R^n $ with $ R/\mathfrak m $ to get an isomorphism of $ R/\mathfrak m $-vector spaces $ (R/\mathfrak m)^m \to (R/\mathfrak m)^n $, which implies $ m = n $ by linear algebra since $ R/\mathfrak m $ is a field.

In fact, however, using Zorn's lemma is unnecessary. One way to see this is by looking at the exterior powers of the modules $ R^n $. The exterior power $ \wedge^n R^n $ is nonzero because the determinant $ (R^n)^n \to R $ is a surjective map that factors through $ \wedge^n R^n $, while $ \wedge^m R^n $ is obviously zero for $ m > n $. Therefore the rank of a free module over a nonzero commutative ring corresponds to its highest order exterior power that doesn't vanish, proving the difficult part of the claim that $ m \neq n $ implies $ R^m \ncong R^n $.

It's common to use the axiom of choice to prove that nonzero commutative rings have the invariant basis number property: in other words, that for a nonzero commutative ring $ R $, the $ R $-modules $ R^m $ and $ R^n $ are isomorphic if and only if $ m = n $.

The most common proof of this uses Zorn's lemma to find a maximal ideal $ \mathfrak m $ of $ R $. We can then tensor any isomorphism $ R^m \to R^n $ with $ R/\mathfrak m $ to get an isomorphism of $ R/\mathfrak m $-vector spaces $ (R/\mathfrak m)^m \to (R/\mathfrak m)^n $, which implies $ m = n $ by linear algebra since $ R/\mathfrak m $ is a field.

In fact, however, using Zorn's lemma is unnecessary. One way to see this is by looking at the exterior powers of the modules $ R^n $. The exterior power $ {\bigwedge}^n R^n $ is nonzero because the determinant $ (R^n)^n \to R $ is a surjective map that factors through $ {\bigwedge}^n R^n $, while $ {\bigwedge}^m R^n $ is obviously zero for $ m > n $. Therefore the rank of a free module over a nonzero commutative ring corresponds to its highest order exterior power that doesn't vanish, proving the difficult part of the claim that $ m \neq n $ implies $ R^m \ncong R^n $.

It's common to use the axiom of choice to prove that nonzero commutative rings have the invariant basis number property: in other words, that for a nonzero commutative ring $ R $, the $ R $-modules $ R^m $ and $ R^n $ are isomorphic if and only if $ m = n $.

The most common proof of this uses Zorn's lemma to find a maximal ideal $ \mathfrak m $ of $ R $. We can then tensor any isomorphism $ R^m \to R^n $ with $ R/\mathfrak m $ to get an isomorphism of $ R/\mathfrak m $-vector spaces $ (R/\mathfrak m)^m \to (R/\mathfrak m)^n $, which implies $ m = n $ by linear algebra since $ R/\mathfrak m $ is a field.

In fact, however, using Zorn's lemma is unnecessary. One way to see this is by looking at the exterior powers of the modules $ R^n $. The exterior power $ \wedge^n R^n $ is nonzero because the determinant $ (R^n)^n \to R $ is a surjective map that factors through $ \wedge^n R^n $, while $ \wedge^m R^n $ is obviously zero for $ m > n $. Therefore the rank of a free module over a nonzero commutative ring corresponds to its highest order exterior product that doesn't vanish, proving the difficult part of the claim that $ m \neq n $ implies $ R^m \ncong R^n $.

It's common to use the axiom of choice to prove that nonzero commutative rings have the invariant basis number property: in other words, that for a nonzero commutative ring $ R $, the $ R $-modules $ R^m $ and $ R^n $ are isomorphic if and only if $ m = n $.

The most common proof of this uses Zorn's lemma to find a maximal ideal $ \mathfrak m $ of $ R $. We can then tensor any isomorphism $ R^m \to R^n $ with $ R/\mathfrak m $ to get an isomorphism of $ R/\mathfrak m $-vector spaces $ (R/\mathfrak m)^m \to (R/\mathfrak m)^n $, which implies $ m = n $ by linear algebra since $ R/\mathfrak m $ is a field.

In fact, however, using Zorn's lemma is unnecessary. One way to see this is by looking at the exterior powers of the modules $ R^n $. The exterior power $ \wedge^n R^n $ is nonzero because the determinant $ (R^n)^n \to R $ is a surjective map that factors through $ \wedge^n R^n $, while $ \wedge^m R^n $ is obviously zero for $ m > n $. Therefore the rank of a free module over a nonzero commutative ring corresponds to its highest order exterior power that doesn't vanish, proving the difficult part of the claim that $ m \neq n $ implies $ R^m \ncong R^n $.