package coq-mathcomp-sum-of-two-square

You can search for identifiers within the package.

in-package search v0.2.0

A proof of Fermat's theorem on sum of two squares. It is the proof that uses gaussian integers. This is done in ssreflect. It contains two file :

Install

md5=1633745a81e8e3941d00ffb7e6e89883

gauss_int.v : the definition of gaussian integers

fermat2.v : the proof of Fermat's theorem

The final statement reads:

===================================================

From mathcomp Require Import all_ssreflect.

From mathcomp.contrib.sum_of_two_square Require Import gauss_int fermat2. Check sum2stest.

sum2stest : forall n : nat, reflect (forall p : nat, prime p -> odd p -> p %| n -> odd (logn p n) -> p %% 4 = 1) (n \is a sum_of_two_square)

===================================================

None

None

None

On This Page