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.0.0.tar.gz
sha256=45ff1fc19ee16d1d97892a54fbbc9864e89fe79b0c7aa3cc9503e44bced5f446

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: 14 Jan 2021

Dev Dependencies (3)

  1. coq-mathcomp-real-closed (>= "1.1.1") | = "dev"
  2. coq-mathcomp-ssreflect (>= "1.11.0" & < "1.13~") | = "dev"
  3. coq (>= "8.10" & < "8.14~") | = "dev"

Used by

None

Conflicts

None