Description: Define class of all
groups. A group is a monoid (df-mnd 17912) 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
(Base‘𝐺) per df-base 16489) and an internal group operation
(notated (+g‘𝐺) per df-plusg 16578). 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 18111), associativity (so
((𝑎+g𝑏)+g𝑐) = (𝑎+g(𝑏+g𝑐)) for any a, b, c, see
grpass 18112), identity (there must be an element 𝑒 =
(0g‘𝐺) such
that 𝑒+g𝑎 = 𝑎+g𝑒 = 𝑎 for any a), and inverse (for each
element a
in the base set, there must be an element 𝑏 = invg𝑎 in the base set
such that 𝑎+g𝑏 = 𝑏+g𝑎 = 𝑒). It can be proven that the identity
element is unique (grpideu 18114). Groups need not be commutative; a
commutative group is an Abelian group (see df-abl 18909). Subgroups can
often be formed from groups, see df-subg 18276. An example of an (Abelian)
group is the set of complex numbers ℂ over
the group operation
+ (addition), as proven in cnaddablx 18988; an Abelian group is a group
as proven in ablgrp 18911. Other structures include groups, including
unital rings (df-ring 19299) and fields (df-field 19505). (Contributed by
NM, 17-Oct-2012.) (Revised by Mario Carneiro,
6-Jan-2015.) |