Some extra material for mathcomp
Lower bound of lcm(1, 2, ..., n)
Definitions and some properties of matroids
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
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 formalisation of Residue Number System
Trivial fact about the ultra hex number
Some facts about addition chain
A note about sorting network is available here.
A note about addition chain is available here.
- Author(s):
- Laurent Théry
- License: MIT License
- Compatible Coq versions: 8.18 or later
- Additional dependencies:
- 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
