# Mathematical Components: Installation

## Install the Base Mathematical Components Libraries

- The installation of Mathematical Components is best 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 be installed
similarly using
`opam install`

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

,`coq-mathcomp-field`

,- etc.

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

) - more to come (using nix)

- various ways of installing using

### Installation Instructions in Other Languages

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

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

### Installation Instructions for Windows 10

- It is possible to install the Mathematical Components libraries on Windows 10 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
- WIP, see INSTALL.md

- See the Mathematical Components' github for more libraries