Fields are exactly commutative division rings

Fields are exactly commutative division rings: A ring $R$ is a field if and only if it is a division ring whose multiplication is commutative (equivalently, $R$ is a commutative ring in which every nonzero element is invertible).

This lemma packages the usual equivalence of “commutative + all nonzero invertible” with the field axioms used throughout algebra and algebraic geometry.