Recently, I have been revising a basic course on noncommutative rings and modules over them. One proposition proven early on is all left modules over $R$ are free iff $R$ is a division ring and an interesting point is that, at least in the standard proofs we were given (and I have seen repeated in various places across this site), both directions use the axiom of choice!
As a quick outline, if $R$ is a division ring then we use Zorn's lemma to find a maximal linearly independent set in any left $R$-module and this is a basis. If $R$ is a ring such that every left $R$-module is free, then we use Zorn to find a maximal left ideal in $R$ and then $R/I$ is a simple left $R$-module so $\text{End}_R(R / I)$ is a division ring and then you show it is isomorphic to $R$ with an explicit isomorphism.
My question is: what are some other interesting examples of "iffs" in mathematics where (at least in the standard proofs or otherwise) both implications use choice? Are there other examples in algebra?
