Metamath Proof Explorer


Table of Contents - 20.43.17.2. Internal binary operations

In this subsection, "internal binary operations" obeying different laws are defined.

  1. cintop
  2. cclintop
  3. cassintop
  4. df-intop
  5. df-clintop
  6. df-assintop
  7. intopval
  8. intop
  9. clintopval
  10. assintopval
  11. assintopmap
  12. isclintop
  13. clintop
  14. assintop
  15. isassintop
  16. clintopcllaw
  17. assintopcllaw
  18. assintopasslaw
  19. assintopass