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