Description: Define class of all
groups. A group is a monoid (df-mnd 14645) 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  is
an algebraic structure formed from a base set of elements (notated
    per df-base 13429) and an internal group operation
(notated  per df-plusg 13497). 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 14773), associativity (so
   for any a, b, c, see
grpass 14774), identity (there must be an element   such
that for
any a), and inverse (for each element a
in the base set, there must be an element   in the base set
such that ).
It can be proven that the identity
element is unique (grpideu 14776). Groups need not be commutative; a
commutative group is an Abelian group (see df-abl 15370). Subgroups can
often be formed from groups, see df-subg 14896. An example of an (Abelian)
group is the set of complex numbers  over the group operation
 (addition),
as proven in cnaddablx 15436; an Abelian group is a group
as proven in ablgrp 15372. Other structures include groups, including
unital rings (df-rng 15618) and fields (df-field 15793). (Contributed by
NM, 17-Oct-2012.) (Revised by Mario Carneiro,
6-Jan-2015.) |
