Example of an abelian group: ⟨Q+, (x,y) ↦ xy/2⟩

The positive rational numbers form with the operation (x,y) ↦ xy/2 an abelian group.

Lemma Qpos_multdiv2_is_CAbGroup : is_CAbGroup Qpos_multdiv2_as_CGroup.

Definition Qpos_multdiv2_as_CAbGroup := Build_CAbGroup
 Qpos_multdiv2_as_CGroup Qpos_multdiv2_is_CAbGroup.