| Mode | Name | Size | |
|---|---|---|---|
| l--------- | AUTHORS | 17 | logplain |
| l--------- | CeCILL-B | 18 | logplain |
| l--------- | INSTALL | 17 | logplain |
| -rw-r--r-- | Make | 234 | logplain |
| -rw-r--r-- | Makefile | 431 | logplain |
| l--------- | README | 16 | logplain |
| -rw-r--r-- | abelian.v | 89277 | logplain |
| -rw-r--r-- | all.v | 456 | logplain |
| -rw-r--r-- | alt.v | 24180 | logplain |
| -rw-r--r-- | burnside_app.v | 48900 | logplain |
| -rw-r--r-- | center.v | 24442 | logplain |
| -rw-r--r-- | commutator.v | 13255 | logplain |
| -rw-r--r-- | extraspecial.v | 41802 | logplain |
| -rw-r--r-- | extremal.v | 122881 | logplain |
| -rw-r--r-- | finmodule.v | 27060 | logplain |
| -rw-r--r-- | frobenius.v | 35569 | logplain |
| -rw-r--r-- | gfunctor.v | 19716 | logplain |
| -rw-r--r-- | gseries.v | 20915 | logplain |
| -rw-r--r-- | hall.v | 42381 | logplain |
| -rw-r--r-- | jordanholder.v | 29590 | logplain |
| -rw-r--r-- | maximal.v | 75684 | logplain |
| -rw-r--r-- | nilpotent.v | 28505 | logplain |
| -rw-r--r-- | opam | 464 | logplain |
| -rw-r--r-- | pgroup.v | 51833 | logplain |
| -rw-r--r-- | primitive_action.v | 14998 | logplain |
| -rw-r--r-- | sylow.v | 27888 | logplain |
 |
index : coq-mathcomp | |
| Library of mathematical components formalized in Coq |
| aboutsummaryrefslogtreecommitdiff |