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.0.tar.gz
sha256=f4f0525d19f8e0527b59383828850dfc5e0503bb2615047ee1cc8cefc0ca4153

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

Published: 29 Oct 2021

Dev Dependencies (3)

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

Used by

None

Conflicts

None