CoRN.model.rings.Qring

Require Export Qabgroup.
Require Import CRings.
Require Import Zring.

Open Local Scope Q_scope.

Example of a ring: ⟨Q,[+],[*]⟩

Because Q forms an abelian group with addition, a monoid with multiplication and it satisfies the distributive law, it is a ring.

Lemma Q_mult_plus_is_dist : distributive Qmult_is_bin_fun Qplus_is_bin_fun.

Definition Q_is_CRing : is_CRing Q_as_CAbGroup 1 Qmult_is_bin_fun.

Definition Q_as_CRing := Build_CRing _ _ _ Q_is_CRing.

Canonical Structure Q_as_CRing.

The following lemmas are used in the proof that Q is Archimeadian.

Lemma injz_Nring : forall n,
nring (R:=Q_as_CRing) n =inject_Z (nring (R:=Z_as_CRing) n).

Lemma injZ_eq : forall x y : Z, x = y -> (inject_Z x:Q_as_CRing )[=]inject_Z y.

Lemma nring_Q : forall n : nat, nring (R:=Q_as_CRing) n =inject_Z n.

Lemma zring_Q : forall z, zring (R:=Q_as_CRing) z =inject_Z z.