Mathematical Components

Pinned Repositories

Abel
A proof of Abel-Ruffini theorem.
Language:Coq28 15 28
algebra-tactics
Ring, field, lra, nra, and psatz tactics for Mathematical Components
Language:Coq33 7 382
analysis
Mathematical Components compliant Analysis Library
Language:Coq215 16 41149
Coq-Combi
Algebraic Combinatorics in Coq
Language:Coq38 11 57
finmap
Finite sets, finite maps, multisets and generic sets
Language:Coq47 15 3228
hierarchy-builder
High level commands to declare a hierarchy based on packed classes
Language:Coq97 16 20323
math-comp
Mathematical Components
Language:Coq605 32 345117
mcb
Mathematical Components (the Book)
Language:TeX141 15 8625
mczify
Micromega tactics for Mathematical Components
Language:Coq25 11 228
odd-order
The formal proof of the Odd Order Theorem
Language:Coq30 15 616

Mathematical Components's Repositories

math-comp/math-comp
Mathematical Components
Language:Coq605 32 345117
math-comp/analysis
Mathematical Components compliant Analysis Library
Language:Coq215 16 41149
math-comp/mcb
Mathematical Components (the Book)
Language:TeX141 15 8625
math-comp/hierarchy-builder
High level commands to declare a hierarchy based on packed classes
Language:Coq97 16 20323
math-comp/finmap
Finite sets, finite maps, multisets and generic sets
Language:Coq47 15 3228
math-comp/Coq-Combi
Algebraic Combinatorics in Coq
Language:Coq38 11 57
math-comp/algebra-tactics
Ring, field, lra, nra, and psatz tactics for Mathematical Components
Language:Coq33 7 382
math-comp/odd-order
The formal proof of the Odd Order Theorem
Language:Coq30 15 616
math-comp/Abel
A proof of Abel-Ruffini theorem.
Language:Coq28 15 28
math-comp/mczify
Micromega tactics for Mathematical Components
Language:Coq25 11 228
math-comp/tutorial_material
proof script associated to tutorial material
Language:Coq17 8 11
math-comp/multinomials
Multinomials for the Mathematical Components library.
Language:Coq14 14 2513
math-comp/real-closed
Theorems for Real Closed Fields
Language:Coq13 12 1511
math-comp/math-comp.github.io
https://math-comp.github.io/
Language:HTML7 13 211
math-comp/POPLmark
Solutions for the POPLmark challenge
Language:Coq7 16 0
math-comp/docker-mathcomp
Docker images of coq-mathcomp [maintainer=@erikmd]
Language:Dockerfile6 11 113
math-comp/bigenough
Asymptotic reasoning with bigenough
Language:Coq4 6 83
math-comp/dioid
A formalization of the algebraic structure of dioid and associated lemmas (including the Nerode lemma).
Language:Coq3 13 02
math-comp/math-comp-nix
Nix support for mathcomp packages
Language:Nix3 5 05
math-comp/mathcomp-history-before-github
The "coqfinitgroup" repository before the switch to github
Language:Coq3 14 0
math-comp/ssr-manual
SSReflect user manual
Language:PostScript3 17 22
math-comp/wiki
general wiki of the math-comp organization
3 13 0
math-comp/pnp
Lecture notes for a short course on proving/programming in Coq via SSReflect.
Language:Coq2 6 0
math-comp/cad
Formalizing Cylindrical Algebraic Decomposition related theories in mathcomp
Language:Coq1 7 02
math-comp/newtonsums
Newton series transformation
Language:Coq0 13 03
math-comp/tools
Experimental toolbox to manage PR in mathcomp
Language:Shell5 02
math-comp/trajectories
Language:Coq7 174