Some extra material for mathcomp

Fibonacci and Lucas numbers

Lower bound of lcm(1, 2, ..., n)

Definitions and some properties of matroids

Rsa algorithm

More lemmas about polynomials

Polynomials modulo

Binary gcd

Nth root for natural number

The aks algorithm the algorithm as in Hing Lun Chan's PhD thesis

The aks correctness proof a transcription of Hing Lun Chan's proof

The proof of Lucas theorem for binomial

A formalisation of 2-player games (in progress)

A formalisation of Fast Fourier Transform

More theorems about tuples

A formalisation of sorting network

A formalisation of bitonic sort

A formalisation of Batcher odd or even sort

A formalisation of Knuth exchange sort

A fun puzzle about a tricky integer function

A port to mathcomp of the elliptic curve of CoqPrime

A formalisation of some sudoku solvers

A formalisation of Montgomery reduction

A note about sorting network is available here.

• Author(s):
  • Laurent Théry
• License: MIT License
• Compatible Coq versions: 8.18 or later
• Additional dependencies:
  • Hierarchy Builder 1.7.0 or later
  • MathComp ssreflect 2.2.0 or later
  • MathComp fingroup 2.2.0 or later
  • MathComp algebra 2.2.0 or later
  • MathComp field 2.2.0 or later
  • MathComp zify 1.5.0+2.0+8.16 or later
  • MathComp Algebra Tactics 1.2.3 or later
• Coq namespace: mathcomp-extra
• Related publication(s): none

To build and install manually, do:

git clone https://github.com/thery/mathcomp-extra.git
cd mathcomp-extra
make   # or make -j <number-of-cores-on-your-machine> 
make install