# Mathematical Components: Installation

## Install the Base Mathematical Components Libraries

### Installation using the opam package manager

- The installation of Mathematical Components can be done using opam, a package manager for OCaml, the programming language with which Coq is implemented.
- Using opam, the installation of the base Mathematical Components library is as simple as this:

opam repo add coq-released https://coq.inria.fr/opam/released opam install coq-mathcomp-ssreflect

- Other base mathematical components libraries can then be installed
similarly using
`opam install`

. The available packages can be found in the Coq package index:`coq-mathcomp-algebra`

,`coq-mathcomp-field`

,`coq-mathcomp-solvable`

,`coq-mathcomp-fingroup`

,`coq-mathcomp-character`

.

- You can find more detailed installation instructions in INSTALL.md
(from the official distribution), this includes:
- various ways of installing using
`opam`

- installation from the source files (using
`make`

) - installation using nix

- various ways of installing using

### Installation using the Coq platform

- The Coq platform is a distribution of Coq together with a selection of libraries including most Mathematical Components libraries. It supports Linux, macOS, and Windows.

### Installation Instructions in Other Languages

- Installation instructions in Japanese, 日本語
- see「パッケージからの設定」for installation using
`opam`

- see「パッケージからの設定」for installation using

### Advanced: Installation Instructions for Windows 10 & 11 using cygwin-opam or WSL

- It is possible to install the Mathematical Components libraries on Windows 10 & 11 using cygwin together with the binary distribution of Coq or together with opam for Windows, or with Windows Subsystem for Linux, as explained for example here

## Other Mathematical Components Libraries

There are already several libraries that build on top of the base Mathematical Components libraries:

- The Four Color theorem
- Available as the opam package
`coq-fourcolor`

- Available as the opam package
- The Odd Order theorem
- Available as the opam package
`coq-mathcomp-odd-order`

- Available as the opam package
- MathComp Analysis
- Available as the opam package
`coq-mathcomp-analysis`

- Available as the opam package
- Abel-Ruffini theorem
- Available as the opam package
`coq-mathcomp-abel`

- Available as the opam package
- Theorems for Real Closed Fields
- Available as the opam package
`coq-mathcomp-real-closed`

- Available as the opam package
- Finite sets, finite maps, multisets and generic sets
- Available as the opam package
`coq-mathcomp-finmap`

- Available as the opam package
- Multinomials for the Mathematical Components library
- Available as the opam package
`coq-mathcomp-multinomials`

- Available as the opam package
- A formal proof of the irrationality of zeta(3), the Apéry constant
- Available as the opam package
`coq-mathcomp-apery`

- Available as the opam package
- See the Mathematical Components' github for more libraries. coq-community also features a number of libraries using Mathematical Components.