Pinned Repositories
Abel
A proof of Abel-Ruffini theorem.
algebra-tactics
Ring, field, lra, nra, and psatz tactics for Mathematical Components
analysis
Mathematical Components compliant Analysis Library
Coq-Combi
Algebraic Combinatorics in Coq
finmap
Finite sets, finite maps, multisets and generic sets
hierarchy-builder
High level commands to declare a hierarchy based on packed classes
math-comp
Mathematical Components
mcb
Mathematical Components (the Book)
mczify
Micromega tactics for Mathematical Components
odd-order
The formal proof of the Odd Order Theorem
Mathematical Components's Repositories
math-comp/math-comp
Mathematical Components
math-comp/analysis
Mathematical Components compliant Analysis Library
math-comp/mcb
Mathematical Components (the Book)
math-comp/hierarchy-builder
High level commands to declare a hierarchy based on packed classes
math-comp/finmap
Finite sets, finite maps, multisets and generic sets
math-comp/Coq-Combi
Algebraic Combinatorics in Coq
math-comp/algebra-tactics
Ring, field, lra, nra, and psatz tactics for Mathematical Components
math-comp/Abel
A proof of Abel-Ruffini theorem.
math-comp/odd-order
The formal proof of the Odd Order Theorem
math-comp/mczify
Micromega tactics for Mathematical Components
math-comp/tutorial_material
proof script associated to tutorial material
math-comp/multinomials
Multinomials for the Mathematical Components library.
math-comp/real-closed
Theorems for Real Closed Fields
math-comp/math-comp.github.io
https://math-comp.github.io/
math-comp/POPLmark
Solutions for the POPLmark challenge
math-comp/docker-mathcomp
Docker images of coq-mathcomp [maintainer=@erikmd]
math-comp/bigenough
Asymptotic reasoning with bigenough
math-comp/dioid
A formalization of the algebraic structure of dioid and associated lemmas (including the Nerode lemma).
math-comp/mathcomp-history-before-github
The "coqfinitgroup" repository before the switch to github
math-comp/ssr-manual
SSReflect user manual
math-comp/wiki
general wiki of the math-comp organization
math-comp/pnp
Lecture notes for a short course on proving/programming in Coq via SSReflect.
math-comp/cad
Formalizing Cylindrical Algebraic Decomposition related theories in mathcomp
math-comp/math-comp-nix
Nix support for mathcomp packages
math-comp/newtonsums
Newton series transformation
math-comp/tools
Experimental toolbox to manage PR in mathcomp
math-comp/trajectories