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
/
CHANGELOG_UNRELEASED.md
Age
Commit message (
Expand
)
Author
2019-11-22
Injectivity lemmas in fintype (#426)
Kazuhiko Sakaguchi
2019-11-22
Added ssrfun theorem `inj_compr` (#432)
Cyril Cohen
2019-11-22
New generalised induction idiom (#434)
Georges Gonthier
2019-11-20
Merge pull request #399 from CohenCyril/ltn_sub
Yves Bertot
2019-11-19
Merge pull request #420 from pi8027/all-lemmas
Cyril Cohen
2019-11-18
fixing CHANGELOG and ltn_pred lemmas
Cyril Cohen
2019-11-18
More arithmetic theorems
Cyril Cohen
2019-11-15
More lemmas on seqs
Florent Hivert
2019-11-15
Add all_filter, all_pmap, and all_allpairsP in seq.v
Kazuhiko Sakaguchi
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-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
add existsPn/forallPn lemmas
Christian Doczkal
2019-11-03
Interface for commutative and commutative-unitary algebras
Florent Hivert
2019-10-30
Change the order of arguments in `ltngtP`
Kazuhiko Sakaguchi
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-16
shifting to CHANGELOG_UNRELEASED
Cyril Cohen
2019-10-07
Merge pull request #384 from pi8027/hierarchy
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-09-30
Generalize `allpairs_catr` to non-`eqType`s
Kazuhiko Sakaguchi
2019-09-30
Euclid theorem for product (#375)
Laurent Théry
2019-09-30
ffact as a product similar to fact_prod (#374)
Laurent Théry
2019-09-16
fermat little theorem
thery
2019-07-10
totient for prime
thery
2019-07-05
feat(finfun.v): Add tuple_of_finfun, finfun_of_tuple & cancel lemmas
Cyril Cohen
2019-06-04
Fixpoint theorems in finset
Cyril Cohen
2019-05-29
reword entry in CHANGELOG_UNRELEASED.md
Anton Trunov
2019-05-29
Move unreleased changelog entries to CHANGELOG_UNRELEASED.md
Anton Trunov