Coq OPAMcoq-mathcomp-sum-of-two-square
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 : 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) ===================================================
opam install coq-mathcomp-sum-of-two-square.1.0.0
- homepage
- https://github.com/thery/twoSquare
- license
- MIT
- bugs tracker
- https://github.com/thery/twoSquare/issues
- dependencies
- coq >= 8.5 & (coq-math-comp >= 1.5 | (coq-mathcomp-ssreflect >= 1.6 & (coq-mathcomp-algebra >= 1.6 & coq-mathcomp-field >= 1.6)))
- source
- https://github.com/thery/twoSquare/archive/v1.0.0.zip
- package
- https://github.com/coq/opam-coq-archive/tree/master/released/packages/coq-mathcomp-sum-of-two-square/coq-mathcomp-sum-of-two-square.1.0.0