package rocq-mathcomp-fingroup
Mathematical Components Library on finite groups
Install
Dune Dependency
Authors
Maintainers
Sources
mathcomp-2.4.0.tar.gz
sha256=6307218d7e434fb6ffc81b9275c673d3f7f1f4884ad59b904abd205c437021a0
Description
This library contains definitions and theorems about finite groups, group quotients, group morphisms, group presentation, group action...
Tags
keyword:small scale reflection keyword:mathematical components keyword:finite groups logpath:mathcomp.fingroupPublished: 15 Apr 2025
Dependencies (1)
-
rocq-mathcomp-ssreflect
= version
Dev Dependencies
None
Used by (7)
-
coq-htt
>= "2.3.0" -
coq-htt-core
>= "2.3.0" -
coq-mathcomp-fingroup
= "2.4.0" -
rocq-mathcomp-algebra
< "2.5.0" -
rocq-mathcomp-classical
< "1.17.0" - rocq-monae
- rocq-rouche-capelli
Conflicts
None
On This Page