| Mode | Name | Size | |
|---|---|---|---|
| -rw-r--r-- | algC.v | 74208 | logplain |
| -rw-r--r-- | algebraics_fundamentals.v | 53565 | logplain |
| -rw-r--r-- | algnum.v | 39299 | logplain |
| -rw-r--r-- | all.v | 289 | logplain |
| -rw-r--r-- | closed_field.v | 24910 | logplain |
| -rw-r--r-- | countalg.v | 49172 | logplain |
| -rw-r--r-- | cyclotomic.v | 15027 | logplain |
| -rw-r--r-- | falgebra.v | 47760 | logplain |
| -rw-r--r-- | fieldext.v | 68189 | logplain |
| -rw-r--r-- | finfield.v | 25951 | logplain |
| -rw-r--r-- | galois.v | 70315 | logplain |
| -rw-r--r-- | separable.v | 44701 | logplain |
 |
index : coq-mathcomp | |
| Library of mathematical components formalized in Coq |
| aboutsummaryrefslogtreecommitdiff |