All Projects → math-comp → multinomials

math-comp / multinomials

Licence: other
Multinomials for the Mathematical Components library.

Programming Languages

Coq
218 projects
Makefile
30231 projects

Projects that are alternatives of or similar to multinomials

finmap
Finite sets, finite maps, multisets and generic sets
Stars: ✭ 45 (+275%)
Mutual labels:  coq, ssreflect, mathcomp
gaia
Implementation of books from Bourbaki's Elements of Mathematics in Coq [maintainer=@thery]
Stars: ✭ 15 (+25%)
Mutual labels:  coq, ssreflect, mathcomp
Actuary
Formalization of the basic actuarial mathematics using Coq
Stars: ✭ 17 (+41.67%)
Mutual labels:  coq, ssreflect, mathcomp
stablesort
Stable sort algorithms and their stability proofs in Coq
Stars: ✭ 19 (+58.33%)
Mutual labels:  coq, ssreflect, mathcomp
Abel
A proof of Abel-Ruffini theorem.
Stars: ✭ 26 (+116.67%)
Mutual labels:  coq, ssreflect, mathcomp
odd-order
The formal proof of the Odd Order Theorem
Stars: ✭ 20 (+66.67%)
Mutual labels:  coq, ssreflect, mathcomp
autosubst
Automation for de Bruijn syntax and substitution in Coq [maintainers=@RalfJung,@co-dan]
Stars: ✭ 41 (+241.67%)
Mutual labels:  coq, ssreflect, mathcomp
coqeal
The Coq Effective Algebra Library [maintainers=@CohenCyril,@proux01]
Stars: ✭ 62 (+416.67%)
Mutual labels:  coq, mathcomp
vericert
A formally verified high-level synthesis tool based on CompCert and written in Coq.
Stars: ✭ 63 (+425%)
Mutual labels:  coq
RiscvSpecFormal
The RiscvSpecKami package provides SiFive's RISC-V processor model. Built using Coq, this processor model can be used for simulation, model checking, and semantics analysis. The RISC-V processor model can be output as Verilog and simulated/synthesized using standard Verilog tools.
Stars: ✭ 69 (+475%)
Mutual labels:  coq
coq-library-undecidability
A library of mechanised undecidability proofs in the Coq proof assistant.
Stars: ✭ 84 (+600%)
Mutual labels:  coq
PolyJuMP.jl
A JuMP extension for Polynomial Optimization
Stars: ✭ 36 (+200%)
Mutual labels:  polynomials
regex-reexamined-coq
No description or website provided.
Stars: ✭ 14 (+16.67%)
Mutual labels:  coq
coq-big-o
A general yet easy-to-use formalization of Big O, Big Theta, and more based on seminormed vector spaces.
Stars: ✭ 31 (+158.33%)
Mutual labels:  coq
coq-art
Coq code and exercises from the Coq'Art book [maintainers=@ybertot,@Casteran]
Stars: ✭ 57 (+375%)
Mutual labels:  coq
tr29124 test
C++ special math functions
Stars: ✭ 16 (+33.33%)
Mutual labels:  polynomials
coq-program-verification-template
Template project for program verification in Coq
Stars: ✭ 26 (+116.67%)
Mutual labels:  coq
LibHyps
A Coq library providing tactics to deal with hypothesis
Stars: ✭ 14 (+16.67%)
Mutual labels:  coq
FreeSpec
A framework for implementing and certifying impure computations in Coq
Stars: ✭ 48 (+300%)
Mutual labels:  coq
mcoq
Mutation analysis tool for Coq verification projects
Stars: ✭ 22 (+83.33%)
Mutual labels:  coq

A Multivariate polynomial Library for the Mathematical Components Library

This library provides a library for monomial algebra,for multivariate polynomials over ring structures and an extended theory for polynomials whose coefficients range over commutative rings and integral domains.

Building and installation instructions

The easiest way to install the latest released version this library is via OPAM:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-mathcomp-multinomials

If you want to install it manually, do:

git clone https://github.com/math-comp/multinomials.git
cd multinomials
make   # or make -j <number-of-cores-on-your-machine> 
make install

Authors

"Pierre-Yves Strub" <[email protected]>

Contributors:

This library is also the result of discussions with:

Note that the project description data, including the texts, logos, images, and/or trademarks, for each open source project belongs to its rightful owner. If you wish to add or remove any projects, please contact us at [email protected].