Abel

Galois theorem formalizer

Formalization of mathematical theorems about solvability and Galois theory for polynomials

A proof of Abel-Ruffini theorem.

GitHub

28 stars
8 watching
8 forks
Language: Coq
last commit: 6 days ago
abel-ruffinicoqgalois-theorymathcompssreflect

Related projects:

Repository Description Stars
math-comp/coq-combi Formalises algebraic combinatorics in Coq using symmetric functions and polynomials 36
math-comp/math-comp A comprehensive repository of formalized mathematical theories based on Coq and SSReflect. 587
thery/mathcomp-extra A collection of reusable mathematical components and algorithms implemented in Coq 5
math-comp/odd-order Verifies a mathematical theorem in finite group theory 25
affeldt-aist/infotheo A Coq formalization of mathematical foundations for information theory and error-correcting codes 64
stepchowfun/proofs A personal repository of formally verified mathematics using the Coq proof assistant 291
math-comp/analysis A comprehensive Coq proof-assistant library for mathematical analysis 206
vafeiadis/hahn A collection of lemmas and tactics about lists and binary relations for a proof assistant 30
charguer/tlc A Coq library providing an alternative set of axioms and type class mechanisms for building and proving mathematical theorems. 38
coq-community/lemma-overloading A Coq library demonstrating design patterns for automated proof automation and canonical structures 26
ilyasergey/pnp A tutorial project on using Coq to mechanize mathematics with dependent types 160
llee454/functional-algebra A Coq formalization of abstract algebra using functional programming style 28
coq-community/coqtail-math A collection of mathematical theorems and tools within the Coq proof assistant 15
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/gaia A Coq implementation of mathematical concepts from N. Bourbaki's Elements of Mathematics 28