package coq-mathcomp-abel

You can search for identifiers within the package.

in-package search v0.2.0

Abel - Ruffini's theorem

Install

Dune Dependency

github.com Edit opam file Versions (3)

Authors

Maintainers

C

Cyril Cohen <cyril.cohen@inria.fr>

Sources

1.2.1.tar.gz

sha256=1f626cff3115794d7753cf2a7a15373579f2ef5d895e8ee5423e4dedae1b2167

Description

This repository contains a proof of Abel - Galois Theorem (equivalence between being solvable by radicals and having a solvable Galois group) and Abel - Ruffini Theorem (unsolvability of quintic equations) in the Coq proof-assistant and using the Mathematical Components library.

Published: 24 Oct 2022

Dependencies (4)

Dev Dependencies (3)

coq-mathcomp-real-closed (>= "1.1.1") | = "dev"
coq-mathcomp-ssreflect (>= "1.12.0" & < "1.16~") | = "dev"
coq (>= "8.10" & < "8.17~") | = "dev"

Used by

None

Conflicts