puiseuxth

Root computation library

Formal proof and implementation of Puiseux's Theorem for computing roots of polynomials.

Formal proof in Coq of Puiseux's Theorem.

GitHub
4 stars
2 watching
0 forks
Language: Coq
last commit: about 2 months ago
Linked from 1 awesome list


Backlinks from these awesome lists:

Related projects:

Repository Description Stars
stepchowfun/proofs A personal repository of formally verified mathematics using the Coq proof assistant 291
fblanqui/color A comprehensive Coq library providing formal definitions and proofs of rewriting theory, lambda-calculus, and termination. 35
coq-community/fourcolor A formal proof of a fundamental result in graph theory using the Coq proof assistant 166
math-comp/abel Formalization of mathematical theorems about solvability and Galois theory for polynomials 28
dschepler/coq-sequent-calculus Formalizations of logical deduction systems using Coq 44
geohot/coq-hardy Formalizing mathematical theorems from Hardy's book in Coq to create a rigorous and reproducible formalization of number theory 53
coq-community/dedekind-reals A formalization of Dedekind reals numbers in the Coq programming language 43
bodigrim/poly A Haskell library for manipulating polynomials with efficient arithmetic operations and scaling. 66
dmxlarchey/coq-kruskal A comprehensive library of constructive Coq proofs for Kruskal's tree theorem and related concepts. 0
lysxia/system-f A formalization of polymorphic lambda calculus with a proof of parametricity theorem. 33
unimath/unimath Formalizes mathematics using the univalent point of view 961
geocoq/geocoq A formalization of geometry using the Coq proof assistant. 186
dmxlarchey/kruskal-veldman A detailed proof of Wim Veldman's tree theorem adaptation in Coq 0
vafeiadis/hahn A collection of lemmas and tactics about lists and binary relations for a proof assistant 30
snu-sf/paco A Coq library for proving properties about stateful systems through parameterized coinduction 43