Description: Define class of all groups. A group is a monoid ( df-mnd ) whose
internal operation is such that every element admits a left inverse
(which can be proven to be a two-sided inverse). Thus, a group G is
an algebraic structure formed from a base set of elements (notated
( BaseG ) per df-base ) and an internal group operation
(notated ( +gG ) per df-plusg ). The operation combines any
two elements of the group base set and must satisfy the 4 group axioms:
closure (the result of the group operation must always be a member of
the base set, see grpcl ), associativity (so
( ( a +g b ) +g c ) = ( a +g ( b +g c ) ) for any a, b, c, see
grpass ), identity (there must be an element e = ( 0gG ) such
that e +g a = a +g e = a for any a), and inverse (for each element a
in the base set, there must be an element b = invg a in the base set
such that a +g b = b +g a = e ). It can be proven that the identity
element is unique ( grpideu ). Groups need not be commutative; a
commutative group is an Abelian group (see df-abl ). Subgroups can
often be formed from groups, see df-subg . An example of an (Abelian)
group is the set of complex numbers CC over the group operation
+ (addition), as proven in cnaddablx ; an Abelian group is a group
as proven in ablgrp . Other structures include groups, including
unital rings ( df-ring ) and fields ( df-field ). (Contributed by NM, 17-Oct-2012)(Revised by Mario Carneiro, 6-Jan-2015)