It is well known that the axioms of a ring R with unity 1 imply that the underlying group must be commutative. 


For if a and b are elements of R, and writing + for the group operation then applying the distributive property one has
$$
\begin{align}
a+a+b+b&=a\*(1+1)+b\*(1+1)\\\\
&=(a+b)\*(1+1)\\\\
&=(a+b)\*1+(a+b)\*1\\\\
&=a+b+a+b,
\end{align}
$$
whence $a+b=b+a$.


For educational purposes, are there more (not only algebraic) examples of such superfluous definitions?



Superfluous definitions
A unique factorization domain is typically defined as:


a domain $D$ such that each non-zero and non-invertible element $d$ can be factored as a product of irreducible elements.


And, for any factorizations $d=u\_1 \dots u\_m$ and $d = v\_1 \dots v\_n$ with irreducibles $u\_i,v\_i$ one has
that $m=n$ and there exists a permutation $\sigma$ of $\{1,\dots, n\}$ such that for all $i$ one has that $u\_i$ and $v\_{\sigma(i)}$ are associated.


Yet, this can be replaced by:


And, for any factorizations $d=u\_1 \dots u\_n$ and $d = v\_1 \dots v\_n$ with irreducibles $u\_i,v\_i$ one has that there exists a permutation $\sigma$ of $\{1,\dots, n\}$ such that for all $i$ one has that $u\_i$ and $v\_{\sigma(i)}$ are associated.


In other words, it is sufficient that all factorizations of an element with the *same number of factors* are essentially equal. The fact that there, then, cannot be any factorization with a different number of factors can be proved and thus not have to be included in the definition.


Side note: If one replaces 'domain' by 'commutative cancellative semigroup with identity' the weakened definition actually is different.


