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 :
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
- "ocaml" "coq" {>= "8.5"} "coq-mathcomp-ssreflect" {>= "1.6" & < "1.7"} "coq-mathcomp-algebra" {>= "1.6" & < "1.7"} "coq-mathcomp-field" {>= "1.6" & < "1.7"}
- 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