index
:
coq-mathcomp
master
Library of mathematical components formalized in Coq
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2019-11-18
Documenting `L` and `R` in `CONTRIBUTING.md`
Cyril Cohen
2019-11-18
More arithmetic theorems
Cyril Cohen
2019-11-18
Merge pull request #381 from hivert/seq
Yves Bertot
2019-11-15
More lemmas on seqs
Florent Hivert
2019-11-15
fix in ssralg (#421)
Cyril Cohen
2019-11-15
Add all_filter, all_pmap, and all_allpairsP in seq.v
Kazuhiko Sakaguchi
2019-11-14
Merge pull request #423 from thery/doc
Yves Bertot
2019-11-14
typo
thery
2019-11-14
fingraph: remove fin_inj_bij lemma as duplicate of injF_bij from fintype (#403)
Anton Trunov
2019-11-14
Lemmas on commutation with big sum and prod (#413)
Florent Hivert
2019-11-14
Update pull_request_template.md
Cyril Cohen
2019-11-14
Update zmodp.v (#411)
Gabriel Taumaturgo
2019-11-14
some information about naming conventions for definitions (wip) (#415)
affeldt-aist
2019-11-14
typo (#412)
Laurent Théry
2019-11-06
Merge pull request #410 from GTaumaturgo/patch-1
Cyril Cohen
2019-11-06
Merge pull request #408 from chdoc/existsPn
Cyril Cohen
2019-11-06
Merge pull request #406 from hivert/algebras
Cyril Cohen
2019-11-04
Update README.md
Gabriel Taumaturgo
2019-11-04
Fixed the documentation
Florent Hivert
2019-11-04
minor revision
Christian Doczkal
2019-11-04
Fixed inheritance of fieldExt / fieldOver / splitting field
Florent Hivert
2019-11-04
add existsPn/forallPn lemmas
Christian Doczkal
2019-11-03
Interface for commutative and commutative-unitary algebras
Florent Hivert
2019-10-31
Merge pull request #378 from pi8027/fix-ltngtP
Cyril Cohen
2019-10-30
Change the order of arguments in `ltngtP`
Kazuhiko Sakaguchi
2019-10-30
Merge pull request #400 from pi8027/scale-type
Cyril Cohen
2019-10-26
Add an explicit type annotation to GRing.scale
Kazuhiko Sakaguchi
2019-10-26
Merge pull request #397 from CohenCyril/remove_addnKC
Laurent Théry
2019-10-25
Removing duplicate lemma `addnKC` (= `addKn`)
Cyril Cohen
2019-10-25
Merge pull request #396 from CohenCyril/edivnD
Laurent Théry
2019-10-25
Instances for empty type. (#393)
Arthur Azevedo de Amorim
2019-10-25
Stability proofs of sort (#358)
Kazuhiko Sakaguchi
2019-10-25
More arithmetic theorems
Cyril Cohen
2019-10-24
Added and generalized arithmetic theorems. (#394)
Cyril Cohen
2019-10-21
Merge pull request #365 from math-comp/ghpages-redirect
Maxime Dénès
2019-10-18
Add build for mathcomp/mathcomp-dev:coq-8.10 (#391)
Erik Martin-Dorel
2019-10-16
Merge pull request #203 from CohenCyril/improving_fintype_bigop
Maxime Dénès
2019-10-16
shifting to CHANGELOG_UNRELEASED
Cyril Cohen
2019-10-16
renaming new `reindex_` lemmas with prefix `big_`
Cyril Cohen
2019-10-16
Improving fintype and bigop
Cyril Cohen
2019-10-16
removing everything but index which redirects to the new page
Cyril Cohen
2019-10-15
Merge pull request #390 from thery/doc
Cyril Cohen
2019-10-14
typo
thery
2019-10-07
Merge pull request #384 from pi8027/hierarchy
Cyril Cohen
2019-10-07
Merge pull request #387 from pi8027/seq-lemmas
Cyril Cohen
2019-10-05
Add flatten_map1 and allpairs_consr
Kazuhiko Sakaguchi
2019-10-02
Fix and improve the test suite and Makefile
Kazuhiko Sakaguchi
2019-10-01
Merge pull request #386 from pi8027/allpairs
Cyril Cohen
2019-09-30
Generalize `allpairs_catr` to non-`eqType`s
Kazuhiko Sakaguchi
2019-09-30
Euclid theorem for product (#375)
Laurent Théry
[prev]
[next]