Metamath Proof Explorer

Table of Contents - 10.1.1. Magmas

According to Wikipedia ("Magma (algebra)", 08-Jan-2020, "In abstract algebra, a magma [...] is a basic kind of algebraic structure. Specifically, a magma consists of a set equipped with a single binary operation. The binary operation must be closed by definition but no other properties are imposed.".

Since the concept of a "binary operation" is used in different variants, these differences are explained in more detail in the following:

With df-mpo, binary operations are defined by a rule, and with df-ov, the value of a binary operation applied to two operands can be expressed. In both cases, the two operands can belong to different sets, and the result can be an element of a third set. However, according to Wikipedia "Binary operation", see (19-Jan-2020), "... a binary operation on a set is a mapping of the elements of the Cartesian product to S: . Because the result of performing the operation on a pair of elements of S is again an element of S, the operation is called a closed binary operation on S (or sometimes expressed as having the property of closure).". To distinguish this more restrictive definition (in Wikipedia and most of the literature) from the general case, binary operations mapping the elements of the Cartesian product are more precisely called internal binary operations. If, in addition, the result is also contained in the set , the operation should be called closed internal binary operation. Therefore, a "binary operation on a set " according to Wikipedia is a "closed internal binary operation" in a more precise terminology. If the sets are different, the operation is explicitly called external binary operation (see Wikipedia

The definition of magmas (, see df-mgm) concentrates on the closure property of the associated operation, and poses no additional restrictions on it. In this way, it is most general and flexible.

  1. cplusf
  2. cmgm
  3. df-plusf
  4. df-mgm
  5. ismgm
  6. ismgmn0
  7. mgmcl
  8. isnmgm
  9. mgmsscl
  10. plusffval
  11. plusfval
  12. plusfeq
  13. plusffn
  14. mgmplusf
  15. issstrmgm
  16. intopsn
  17. mgmb1mgm1
  18. mgm0
  19. mgm0b
  20. mgm1
  21. opifismgm