Hi, Mr. Bantchev.

Yes, all of the definitions I pointed in this post have redundancy. Your remark is definitely a good (interesting) one.

However, for me, minimality is not as important as logical correctness and usability.

I tried to show that the usual definition is not logically correct. And for me, logical correctness in the context of modern Mathematics (not just in the context of Mathematical logic) means that if one definition is given in a natural language it should also be straightforward to be given in a formally correct way. And as I showed the translation of the usual definition requires non-trivial translation (the statement that there exists an identity and that there is an “inverse” of each element should be combined together).

And of course. the reason why the usual definition is not logically correct is that the two parts are separated with the belief that in this way things are easier. And this for me rings a bell for a Math smell. Again because in order for this definition to work a statement should be proven along with the definition.