Package: wnpp X-Debbugs-Cc: debian-de...@lists.debian.org Owner: Julien Puydt <jpu...@debian.org> X-Debbugs-Cc: debian-ocaml-ma...@lists.debian.org Severity: wishlist
* Package name : mathcomp-abel Version : 1.2.1 Upstream Author : Sophie Bernard, Cyril Cohen, Assia Mahboubi, Pierre-Yves Strub * URL : https://github.com/math-comp/Abel * License : CeCILL-B Programming Lang: Coq Description : Abel-Galois and Abel-Ruffini theorems for Mathematical Components This package provides proofs of the Abel-Galois (solvability by radicals and solvability of the Galois group) and of the Abel-Ruffini theorem (general unsolvability of the quintic equations) using the Mathematical Components library. . The Mathematical Components library is a coherent repository of general-purpose formalized mathematical theories for the Coq proof assistant. I plan to support it within the Debian Ocaml Maintainers team, alongside the other Coq-related packages we have. Cheers, J.Puydt