Mathematical Components

All

27 repositories

analysis
Public
Mathematical Components compliant Analysis Library
coq ssreflect mathcomp analysis
Rocq Prover
•
Other
•59•221•85•47•Updated Aug 7, 2025Aug 7, 2025
algebra-tactics
Public
Ring, field, lra, nra, and psatz tactics for Mathematical Components
proof-automation ssreflect mathcomp elpi coq
Rocq Prover
•4•34•14•0•Updated Jul 29, 2025Jul 29, 2025
hierarchy-builder
Public
High level commands to declare a hierarchy based on packed classes
coq mathcomp elpi
Rocq Prover
•
MIT License
•25•100•85•22•Updated Jul 27, 2025Jul 27, 2025
math-comp
Public
Mathematical Components
coq ssreflect mathcomp
Rocq Prover
•
Other
•124•633•118•37•Updated Jul 25, 2025Jul 25, 2025
math-comp.github.io
Public
https://math-comp.github.io/
HTML
•10•7•0•0•Updated Jul 10, 2025Jul 10, 2025
finmap
Public
Finite sets, finite maps, multisets and generic sets
coq ssreflect finite-sets mathcomp
Rocq Prover
•29•49•12•2•Updated Jul 4, 2025Jul 4, 2025
odd-order
Public
The formal proof of the Odd Order Theorem
coq ssreflect mathcomp odd-order-theorem feit-thompson-theorem
Rocq Prover
•16•31•1•4•Updated Jul 3, 2025Jul 3, 2025
trajectories
Public
Rocq Prover
•5•0•8•0•Updated Jul 1, 2025Jul 1, 2025
multinomials
Public
Multinomials for the Mathematical Components library.
polynomials mathcomp coq ssreflect
Rocq Prover
•
Other
•13•14•4•6•Updated Jun 27, 2025Jun 27, 2025
Abel
Public
A proof of Abel-Ruffini theorem.
coq ssreflect galois-theory abel-ruffini mathcomp
Rocq Prover
•8•29•1•9•Updated Jun 27, 2025Jun 27, 2025
real-closed
Public
Theorems for Real Closed Fields
coq ssreflect mathcomp real-closed-fields
Rocq Prover
•11•13•6•2•Updated Jun 27, 2025Jun 27, 2025
mczify
Public
Micromega tactics for Mathematical Components
coq proof-automation ssreflect mathcomp
Coq
•9•25•4•0•Updated May 12, 2025May 12, 2025
bigenough
Public
Asymptotic reasoning with bigenough
coq ssreflect mathcomp
Coq
•3•4•0•0•Updated May 9, 2025May 9, 2025
docker-mathcomp
Public
Docker images of coq-mathcomp [maintainer=@erikmd]
dockerfile ci coq opam mathcomp docker-image
Dockerfile
•
BSD 3-Clause "New" or "Revised" License
•3•6•3•1•Updated May 2, 2025May 2, 2025
tools
Public
Experimental toolbox to manage PR in mathcomp
Shell
•
MIT License
•2•0•0•1•Updated Apr 8, 2025Apr 8, 2025
dioid
Public
A formalization of the algebraic structure of dioid and associated lemmas (including the Nerode lemma).
coq mathcomp
Coq
•
Other
•2•3•0•0•Updated Feb 27, 2025Feb 27, 2025
Coq-Combi
Public
Algebraic Combinatorics in Coq
Coq
•
GNU General Public License v3.0
•8•38•1•2•Updated Jan 21, 2025Jan 21, 2025
cad
Public
Formalizing Cylindrical Algebraic Decomposition related theories in mathcomp
coq ssreflect mathcomp
Coq
•
GNU Lesser General Public License v3.0
•2•0•0•2•Updated Dec 12, 2024Dec 12, 2024
math-comp-nix
Public
Nix support for mathcomp packages
Nix
•
GNU General Public License v3.0
•4•3•0•6•Updated Mar 7, 2024Mar 7, 2024
mcb
Public
Mathematical Components (the Book)
TeX
•
Other
•26•146•37•1•Updated Nov 14, 2023Nov 14, 2023
tutorial_material
Public
proof script associated to tutorial material
Coq
•1•17•1•0•Updated Oct 29, 2023Oct 29, 2023
mathcomp-history-before-github
Public archive
The "coqfinitgroup" repository before the switch to github
Coq
•0•3•0•0•Updated Mar 25, 2020Mar 25, 2020
newtonsums
Public
Newton series transformation
coq mathcomp
Coq
•3•0•0•1•Updated Nov 10, 2019Nov 10, 2019
POPLmark
Public
Solutions for the POPLmark challenge
coq ssreflect mathcomp
Coq
•0•7•0•0•Updated Nov 9, 2019Nov 9, 2019
wiki
Public archive
general wiki of the math-comp organization
0•3•0•0•Updated Dec 10, 2018Dec 10, 2018
ssr-manual
Public archive
SSReflect user manual
PostScript
•2•3•2•0•Updated Feb 27, 2018Feb 27, 2018
pnp
Public
Lecture notes for a short course on proving/programming in Coq via SSReflect.
Coq
•19•2•0•0•Updated Dec 22, 2016Dec 22, 2016