CoRN.model.monoids.Qmonoid

Require Export Qsemigroup.
Require Import CMonoids.

Open Local Scope Q_scope.

Examples of a monoid: ⟨Q,[+]⟩ and ⟨Q,[*]⟩

⟨Q,[+]⟩

The rational numbers form with addition a CMonoid. QZERO is the unit.

Lemma ZEROQ_as_rht_unit3 : is_rht_unit (S:=Q_as_CSetoid) Qplus_is_bin_fun 0.
Proof. repeat intro. apply Qplus_0_r. Qed.

Lemma ZEROQ_as_lft_unit3 : is_lft_unit (S:=Q_as_CSetoid) Qplus_is_bin_fun 0.
Proof. repeat intro. apply Qplus_0_l. Qed.

Definition Q_is_CMonoid := Build_is_CMonoid
Q_as_CSemiGroup _ ZEROQ_as_rht_unit3 ZEROQ_as_lft_unit3.

Definition Q_as_CMonoid := Build_CMonoid Q_as_CSemiGroup _ Q_is_CMonoid.

Canonical Structure Q_as_CMonoid.

⟨Q,[*]⟩

Also with multiplication Q forms a CMonoid. Here, the unit is QONE.

Lemma ONEQ_as_rht_unit : is_rht_unit (S:=Q_as_CSetoid) Qmult_is_bin_fun 1.
Proof. repeat intro. apply Qmult_1_r. Qed.

Lemma ONEQ_as_lft_unit : is_lft_unit (S:=Q_as_CSetoid) Qmult_is_bin_fun 1.
Proof. repeat intro. apply Qmult_1_l. Qed.

Definition Q_mul_is_CMonoid := Build_is_CMonoid
Q_mul_as_CSemiGroup _ ONEQ_as_rht_unit ONEQ_as_lft_unit.

Definition Q_mul_as_CMonoid := Build_CMonoid
Q_mul_as_CSemiGroup _ Q_mul_is_CMonoid.