| Mode | Name | Size | |
|---|---|---|---|
| l--------- | AUTHORS | 13 | logplain |
| l--------- | CeCILL-B | 14 | logplain |
| l--------- | INSTALL.md | 16 | logplain |
| -rw-r--r-- | Make | 252 | logplain |
| -rw-r--r-- | Makefile | 171 | logplain |
| l--------- | README.md | 15 | logplain |
| -rw-r--r-- | abelian.v | 89616 | logplain |
| -rw-r--r-- | all_solvable.v | 479 | logplain |
| -rw-r--r-- | alt.v | 24347 | logplain |
| -rw-r--r-- | burnside_app.v | 48948 | logplain |
| -rw-r--r-- | center.v | 24540 | logplain |
| -rw-r--r-- | commutator.v | 13379 | logplain |
| -rw-r--r-- | cyclic.v | 33456 | logplain |
| -rw-r--r-- | descr | 127 | logplain |
| -rw-r--r-- | extraspecial.v | 41959 | logplain |
| -rw-r--r-- | extremal.v | 122686 | logplain |
| -rw-r--r-- | finmodule.v | 27222 | logplain |
| -rw-r--r-- | frobenius.v | 35396 | logplain |
| -rw-r--r-- | gfunctor.v | 20390 | logplain |
| -rw-r--r-- | gseries.v | 20749 | logplain |
| -rw-r--r-- | hall.v | 42506 | logplain |
| -rw-r--r-- | jordanholder.v | 29675 | logplain |
| -rw-r--r-- | maximal.v | 75019 | logplain |
| -rw-r--r-- | nilpotent.v | 28361 | logplain |
| -rw-r--r-- | opam | 988 | logplain |
| -rw-r--r-- | pgroup.v | 51255 | logplain |
| -rw-r--r-- | primitive_action.v | 15009 | logplain |
| -rw-r--r-- | sylow.v | 27993 | logplain |
 |
index : coq-mathcomp | |
| Library of mathematical components formalized in Coq |
| aboutsummaryrefslogtreecommitdiff |