Preliminaries

Let's extend the library on rings and algebraic numbers with some easy lemmas first.

Question -2: prove that if a product of natural numbers is 1 then each factor is 1.

Note that we do not consider nat but the copy of nat which is embeded in the algebraic numbers algC. The theorem already exists for nat, and we suggest you use a compatibility lemma numbers between nat and Cnat

Question -1: The real part of product

Question 0: The imaginary part of product

---

The ring of Gauss integers

• Ref: exercices de mathematiques oraux X-ENS algebre 1
• Exercice 3.10. ENS Lyon

First we define a predicate for the algebraic numbers which are gauss integers.

Question 1: Prove that integers are gauss integers

Question 2: Prove that gauss integers form a subfield

There follows the boilerplate to use the proof GI_subring in order to canonically provide a subring structure to the predicate gaussInteger.

Finally, we define the type of Gauss Integer, as a sigma type of algebraic numbers. We soon prove that this is in fact a sub type.

We make the defining property of GI a Hint

We provide the subtype property.

• This makes it possible to use the generic operator val to get an algC from a Gauss Integer.

We deduce that the real and imaginary parts of a GI are integers

We provide a ring structure to the type GI, using the subring canonical property for the predicate gaussInteger

• Now we build the unitRing and comUnitRing structure of gauss integers. Contrarily to the previous structures, the operator is not the same as on algebraics. Indeed the invertible algebraics are not necessarily invertible gauss integers.
• Hence, we define the inverse of gauss integers as follow : if the algebraic inverse happens to be a gauss integer we recover the proof and package it together with the element and get a gauss integer, otherwise, we default to the identity.
• A gauss integer is invertible if the algbraic inverse is a gauss integer.

Question 3: prove a few facts in order to find a comUnitRingMixin

for GI, and then instantiate the interfaces of unitRingType and comUnitRingType.

Question 4: Show that gauss integers are stable by conjugation.

We use this fact to build the conjugation of a gauss Integers

We now define the norm (stasm) for gauss integer, we don't need to specialize it to gauss integer so we define it over algebraic numbers instead.

Question 4: Show that the gaussNorm of x is the square of the complex modulus of x

Question 5: Show that the gaussNorm of an gauss integer is a natural number.

Question 6: Show that gaussNorm is multiplicative (on all algC).

Question 7: Find the invertible elements of GI

• This is question 1 of the CPGE exercice
• Suggested strategy: sketch the proof on a paper first, don't let Coq divert you from your proofsketch

Question 8: Prove that GI euclidean for the stasm gaussNorm.

• i.e. ∀ (a, b) ∈ GI × GI*, ∃ (q, r) ∈ GI² s.t. a = q b + r and φ(r) < φ(b)
• This is question 2 of the CPGE exercice
• Suggested strategy: sketch the proof on a paper first, don't let Coq divert you from your proofsketch

load script