libcoq-mathcomp-solvable

Description

The Mathematical Components Library is an extensive and coherent repository of formalized mathematical theories. It is based on the Coq proof assistant, powered with the Coq/SSReflect language.

These formal theories cover a wide spectrum of topics, ranging from the formal theory of general-purpose data structures like lists, prime numbers or finite graphs, to advanced topics in algebra.

The formalization technique adopted in the library, called "small scale reflection", leverages the higher-order nature of Coq's underlying logic to provide effective automation for many small, clerical proof steps. This is often accomplished by restating ("reflecting") problems in a more concrete form, hence the name. For example, arithmetic comparison is not an abstract predicate, but rather a function computing a Boolean.

This package installs the second finite groups theory part of the library (abelian groups, center, commutator, Jordan-Holder series, Sylow theorems...).

---

Upload more screenshots

Please help extend the collection of screenshots. Just make a screenshot and upload it here. You don't need to register or anything.

Upload a screenshot

Hint: upload an image here from your clipboard with Ctrl-V

---

Homepage

https://math-comp.github.io/math-comp/

---

Install this software package

If the package is available for the distribution you are currently using on your computer then install the software by clicking on…

Install libcoq-mathcomp-solvable