If $AB=I$ implies $BA=I$ for square matrices over a field K, why do we define inverse matrix in such way?

Question

Let $A$ be a square matrix over a field $K$ and $I$ the identity matrix. The inverse matrix of $A$ (when it exists) is a square matrix $B$ such that $\begin{equation}AB=I=BA\end{equation}$. It can proved that $AB=I$ implies $BA=I$ for square matrices over a field, so why don't why just define inverse with one of those conditions instead of both (either $AB=I$ or $BA=I$)? I mean like: A square matrix $A$ over a field $K$ is said to be invertible if there exists a square matrix $B$ such that $AB=I$.

Answer 1

Turned Ian's answer in the comments to a community wiki answer.

We abbreviate "there exists $B$ such that $AB =I$" as "$A$ has a right inverse" and we abbreviate "there exists $B$ such that $BA =I$" as "$A$ has a left inverse". We say an inverse is a left and right inverse. In this definition framework, it is a theorem that if $A$ is square and has a left inverse then that left inverse is a right inverse, and vice versa. We don't need to bake that into the definition. In general, you don't want your definitions to rely on theorems.