package coq-pocklington
Pocklington's criterion in Coq
Install
Dune Dependency
Authors
Maintainers
Sources
v8.12.0.tar.gz
sha512=e17402d9719321c48bebc41030a5d36f8e1c0e31c3ed399bdce1d2c9a858d02c7890c70dddcc866b8d1937bf44b95516b149a9683908a4920de7cd04e6bd182e
Description
Coq formalization of Pocklington's criterion for checking primality for large natural numbers. Includes a formal proof of Fermat's little theorem.
Tags
category:Mathematics/Arithmetic and Number Theory/Number theory keyword:Pocklington keyword:number theory keyword:prime numbers keyword:primality keyword:Fermat's little theorem logpath:Pocklington date:2021-01-01Published: 02 Jan 2021
Dependencies (1)
-
coq
>= "8.7" & < "8.19~"
Dev Dependencies
None
Used by (1)
-
coq-goedel
>= "8.12.0"
Conflicts
None
On This Page