One-sided group axioms criterion (source code)

= One-sided group axioms criterion

An <associative> <binary operation> $*$ on a nonempty <set> $X$ makes $X$ a <group> if there is $e\in X$ with $x*e=x$ for every $x$, and every $x$ has some $z$ with $x*z=e$. No left <identity element> or left <inverse element> assumption is needed. First, an <idempotent element of a semigroup> $y$ satisfies $y=e$: choose $z$ with $y*z=e$ and compute $y=y*e=y*(y*z)=(y*y)*z=y*z=e$. If $x*z=e$, then $(z*x)*(z*x)=(z*(x*z))*x=(z*e)*x=z*x$, so $z*x=e$ by the previous observation. Finally, $e*x=(x*z)*x=x*(z*x)=x*e=x$. Thus all <group axioms> follow.