index
:
coq-mathcomp
master
Library of mathematical components formalized in Coq
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
mathcomp
/
algebra
/
ssralg.v
Age
Commit message (
Expand
)
Author
2018-07-14
Laurent's simplifications
Cyril Cohen
2018-07-04
small generalizations in poly
Cyril Cohen
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
running semi-automated linting on the whole library
Cyril Cohen
2017-12-14
Using x * y = 1 and x / y = 1 to derive the inverse
Cyril Cohen
2017-11-27
following @ggonthier remark.
Cyril Cohen
2017-11-23
Add addrKA and subrKA (addrK and addrNK modulo Associativity)
Cyril Cohen
2016-11-07
update copyright banner
Assia Mahboubi
2016-08-25
Enriched numClosedFieldType so that it factors a lot of theory from both comp...
Cyril Cohen
2015-12-04
Remove more redundant power type structures
Georges Gonthier
2015-12-04
Add missing export
Georges Gonthier
2015-07-28
update copyright banner
Enrico Tassi
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-03-09
Initial commit
Enrico Tassi