Mathematical Components

Mathematical Components (the Book)

Mathematical Components compliant Analysis Library

Mathematical Components

Finite sets, finite maps, multisets and generic sets

A proof of Abel-Ruffini theorem.

Micromega tactics for Mathematical Components

Ring, field, lra, nra, and psatz tactics for Mathematical Components

The formal proof of the Odd Order Theorem

Theorems for Real Closed Fields

Multinomials for the Mathematical Components library.

Docker images of coq-mathcomp [maintainer=?]

High level commands to declare a hierarchy based on packed classes

Algebraic Combinatorics in Coq

https://math-comp.github.io/

Asymptotic reasoning with bigenough

No description provided.

Formalizing Cylindrical Algebraic Decomposition related theories in mathcomp

Solutions for the POPLmark challenge

A formalization of the algebraic structure of dioid and associated lemmas (including the Nerode lemma).

Newton series transformation

Experimental toolbox to manage PR in mathcomp

Nix support for mathcomp packages

SSReflect user manual

The "coqfinitgroup" repository before the switch to github

proof script associated to tutorial material

Lecture notes for a short course on proving/programming in Coq via SSReflect.

general wiki of the math-comp organization