Metamath Proof Explorer
Table of Contents - 20.43.17.2. Internal binary operations
In this subsection, "internal binary operations" obeying different laws are
defined.
- cintop
- cclintop
- cassintop
- df-intop
- df-clintop
- df-assintop
- intopval
- intop
- clintopval
- assintopval
- assintopmap
- isclintop
- clintop
- assintop
- isassintop
- clintopcllaw
- assintopcllaw
- assintopasslaw
- assintopass