Metamath Proof Explorer


Table of Contents - 10.1.2. Identity elements

According to Wikipedia ("Identity element", 7-Feb-2020, https://en.wikipedia.org/wiki/Identity_element): "In mathematics, an identity element, or neutral element, is a special type of element of a set with respect to a binary operation on that set, which leaves any element of the set unchanged when combined with it.". Or in more detail "... an element e of S is called a left identity if e * a = a for all a in S, and a right identity if a * e = a for all a in S. If e is both a left identity and a right identity, then it is called a two-sided identity, or simply an identity." We concentrate on two-sided identities in the following. The existence of an identity (an identity is unique if it exists, see mgmidmo) is an important property of monoids (see mndid), and therefore also for groups (see grpid), but also for magmas not required to be associative. Magmas with an identity element are called "unital magmas" (see Definition 2 in [BourbakiAlg1] p. 12) or, if the magmas are cancellative, "loops" (see definition in [Bruck] p. 15).

In the context of extensible structures, the identity element (of any magma ) is defined as "group identity element" , see df-0g. Related theorems which are already valid for magmas are provided in the following.

  1. mgmidmo
  2. grpidval
  3. grpidpropd
  4. fn0g
  5. 0g0
  6. ismgmid
  7. mgmidcl
  8. mgmlrid
  9. ismgmid2
  10. lidrideqd
  11. lidrididd
  12. grpidd
  13. mgmidsssn0
  14. grpinvalem
  15. grpinva
  16. grprida