Left identity, right identity, and two-sided identity for a binary operation

Let $\ast$ be a binary operation on a set $S$ (Binary operation on a set; associativity, commutativity, and a subset closed under the operation) and let $e\in S$. Then $e$ is

• a left identity for $\ast$ when $e\ast x=x$ for every $x\in S$;
• a right identity for $\ast$ when $x\ast e=x$ for every $x\in S$;
• a two-sided identity, or simply an identity, when it is both.

• The three notions are genuinely different for a general operation, and the library keeps them apart deliberately: several existing items prove the two sides separately. For addition on $\mathbb{N}$, for instance, $n+0=n$ holds by the defining recursion (Addition of natural numbers) while $0+n=n$ is a theorem proved by induction (Left identity for addition).

• A structure can have many left identities and no right identity, so "the identity" is not legitimate language until uniqueness is available. That is A left identity and a right identity for the same binary operation are equal; hence there is at most one two-sided identity, proved next, and it is the item that licenses the definite article everywhere below.