Description: Define class of all
groups. A group is a monoid (df-mnd 17655) 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 16235) and an internal group operation
(notated (+g‘𝐺) per df-plusg 16325). 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 17791), associativity (so
((𝑎+g𝑏)+g𝑐) = (𝑎+g(𝑏+g𝑐)) for any a, b, c, see
grpass 17792), 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 17794). Groups need not be commutative; a
commutative group is an Abelian group (see df-abl 18556). Subgroups can
often be formed from groups, see df-subg 17949. An example of an (Abelian)
group is the set of complex numbers ℂ over
the group operation
+ (addition), as proven in cnaddablx 18631; an Abelian group is a group
as proven in ablgrp 18558. Other structures include groups, including
unital rings (df-ring 18910) and fields (df-field 19113). (Contributed by
NM, 17-Oct-2012.) (Revised by Mario Carneiro,
6-Jan-2015.) |