Metamath Proof Explorer


Table of Contents - 20.43.17.1. Laws for internal binary operations

In this subsection, the "laws" applicable for "binary operations" according to the definition in [Hall] p. 1 and [BourbakiAlg1] p. 1, p. 4 and p. 7 are defined. These laws are called "internal laws" in [BourbakiAlg1] p. xxi.

  1. ccllaw
  2. casslaw
  3. ccomlaw
  4. df-cllaw
  5. df-comlaw
  6. df-asslaw
  7. iscllaw
  8. iscomlaw
  9. clcllaw
  10. isasslaw
  11. asslawass
  12. mgmplusgiopALT
  13. sgrpplusgaopALT