package coq-mathcomp-abel

  1. Overview
  2. No Docs
Abel - Ruffini's theorem

Install

Dune Dependency

github.com Edit opam file Versions (3)

Authors

  1. S
    Sophie Bernard
  2. C
    Cyril Cohen
  3. A
    Assia Mahboubi
  4. P
    Pierre-Yves Strub

Maintainers

  1. 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.

Tags

keyword:algebra keyword:Galois keyword:Abel Ruffini keyword:unsolvability of quintincs logpath:Abel date:2022-07-13

Published: 24 Oct 2022

Dev Dependencies (3)

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

Used by

None

Conflicts

None