| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-07-14 | updated proposition for big_prod_seq_eq1 | Cyril Cohen | |
| 2018-07-14 | Laurent's simplifications | Cyril Cohen | |
| 2018-07-04 | small generalizations in poly | Cyril Cohen | |
| 2018-04-20 | fix symlinks to README, INSTALL and LICENSE | Enrico Tassi | |
| 2018-03-04 | Change deprecated Arguments Scope to Arguments | Jasper Hugunin | |
| 2018-02-21 | Change Implicit Arguments to Arguments in algebra | Jasper Hugunin | |
| 2018-02-06 | fixing things that @ggonthier and @ybertot spotted and some I spotted | Cyril Cohen | |
| 2018-02-06 | running semi-automated linting on the whole library | Cyril Cohen | |
| 2018-01-26 | Merge pull request #171 from CohenCyril/mxdirect_delta | Cyril Cohen | |
| The spaces generated by some delta_mx are in a direct sum | |||
| 2017-12-20 | Merge pull request #172 from CohenCyril/row_mx_eq0 | Assia Mahboubi | |
| Adding row/col/block_mx_eq0 | |||
| 2017-12-14 | The spaces generated by some delta_mx are in a direct sum | Cyril Cohen | |
| proof by @ggonthier | |||
| 2017-12-14 | Using x * y = 1 and x / y = 1 to derive the inverse | Cyril Cohen | |
| fixes #169 | |||
| 2017-12-12 | Adding row/col/block_mx_eq0 | Cyril Cohen | |
| 2017-11-27 | following @ggonthier remark. | Cyril Cohen | |
| 2017-11-23 | Add addrKA and subrKA (addrK and addrNK modulo Associativity) | Cyril Cohen | |
| 2017-10-30 | Fix obsolete vernacular syntax for locality. | Maxime Dénès | |
| It was emitting a deprecation warning and will soon be removed from Coq. | |||
| 2017-10-23 | Remove compatibility with Coq.8.4 (and compatibility hacks that went with it) | Cyril Cohen | |
| 2017-10-23 | Merge pull request #145 from CohenCyril/new-packager | Cyril Cohen | |
| New packager | |||
| 2017-10-19 | fixed homepage | Cyril Cohen | |
| 2017-10-10 | fix building with make flags | Ralf Jung | |
| Fixes #139 | |||
| 2017-02-04 | adding rquot_comRingType | Cyril Cohen | |
| 2016-11-17 | Merge remote-tracking branch 'upstream/master' into fixdoc | Florent Hivert | |
| 2016-11-16 | Fixes the doc of mxalgebra | Florent Hivert | |
| 2016-11-07 | update copyright banner | Assia Mahboubi | |
| 2016-10-24 | wip shorter proof dec factor theorems | Cyril Cohen | |
| 2016-08-25 | Factor theorem for decidable fields, (inspired by PY Strub) | Cyril Cohen | |
| 2016-08-25 | Enriched numClosedFieldType so that it factors a lot of theory from both ↵ | Cyril Cohen | |
| complex and algC. The definitions of 'i, conjC, Re, Im, n.-root, sqrtC and their theory have been moved to the numClosedFieldType structure in ssrnum. This covers boths the uses in algC and complex.v. To that end the numClosedFieldType structure has been enriched with conjugation and 'i. Note that 'i can be deduced from the property of algebraic closure and is only here to let the user chose which definitional equality should hold on 'i. Same thing for conjC that could be written `|x|^+2/x, the only nontrivial (up to my knowledge) property is the fact that conjugation is a ring morphism. | |||
| 2016-03-15 | Merge pull request #34 from strub/master | Enrico | |
| all_algebra now exports zmodp | |||
| 2016-03-15 | all_algebra now exports zmodp | Pierre-Yves Strub | |
| 2016-02-06 | typo in int divn1 -> divz1 | thery | |
| 2015-12-12 | switch ":" to "-" | Cyril Cohen | |
| 2015-12-04 | Add finLmodType, finLalgType and finAlgType instances | Georges Gonthier | |
| 2015-12-04 | Remove more redundant power type structures | Georges Gonthier | |
| 2015-12-04 | Correct join values to baseFingroupType | Georges Gonthier | |
| These were all GRing.Zmodule.sort, instead of the corresponding sort in GRing (Ring.sort, Comin.sort, etc). | |||
| 2015-12-04 | Add missing export | Georges Gonthier | |
| 2015-11-10 | fix INSTALL symlinks | Enrico Tassi | |
| 2015-07-28 | update copyright banner | Enrico Tassi | |
| 2015-07-22 | forgotten import | Cyril Cohen | |
| 2015-07-22 | remove duplicate fields | Cyril Cohen | |
| 2015-07-22 | make the opam package meta data | Cyril Cohen | |
| 2015-07-21 | update opam meta-data | Cyril Cohen | |
| 2015-07-18 | update to preserve backward compatibility with v8.4 | Cyril Cohen | |
| 2015-07-17 | Updating files + reorganizing everything | Cyril Cohen | |
| 2015-04-09 | Using the From X Require Y for v8.4 | Cyril Cohen | |
| 2015-04-08 | packaging for v8.5 | Cyril Cohen | |
| 2015-04-08 | makefiles that are version dependent | Cyril Cohen | |
| 2015-03-19 | packaging fingroup and algebra | Cyril Cohen | |
| The files zmodp and cyclic in fingroup had dependecies in algebra so I put them there. I'm not convinced it's the best solution to this problem. Maybe more subdivisions in algebra would bring a better solution? (Maybe we should send the whole problem to a solver? :P) | |||
| 2015-03-09 | Initial commit | Enrico Tassi | |
 |
index : coq-mathcomp | |
| Library of mathematical components formalized in Coq |
| aboutsummaryrefslogtreecommitdiff |