Example of a semi-group: ⟨
Q
+
,(x,y) ↦ xy/2⟩
The positive rationals form with the operation (x,y) ↦ xy/2 a CSemiGroup.
Definition
Qpos_multdiv2_as_CSemiGroup
:=
Build_CSemiGroup
_
multdiv2
associative_multdiv2
.