package coq-pocklington

  1. Overview
  2. No Docs
Pocklington's criterion in Coq

Install

Dune Dependency

github.com Edit opam file Versions (7)

Authors

  1. O
    Olga Caprotti
  2. M
    Martijn Oostdijk

Maintainers

  1. P
    palmskog@gmail.com

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-01

Published: 02 Jan 2021

Dependencies (1)

  1. coq >= "8.7" & < "8.19~"

Dev Dependencies

None

Used by (1)

  1. coq-goedel >= "8.12.0"

Conflicts

None