Example of an abelian group: ⟨Q,+⟩


Addition is commutative, so the rationals form with the addition a CAbGroup.

Lemma Q_is_CAbGroup : is_CAbGroup Q_as_CGroup.

Definition Q_as_CAbGroup := Build_CAbGroup Q_as_CGroup Q_is_CAbGroup.

Canonical Structure Q_as_CAbGroup.