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
/
ssreflect
/
binomial.v
Age
Commit message (
Expand
)
Author
2020-09-29
rename mem_imset to imset_f (with deprecation)
Christian Doczkal
2020-05-16
A few more revisions
Kazuhiko Sakaguchi
2020-05-13
Revise proofs in ssreflect/*.v
Kazuhiko Sakaguchi
2020-04-08
fix typos in documentation: formulae
Antonio Nikishaev
2020-04-08
fix typos in documentation: text
Antonio Nikishaev
2019-12-28
Refactoring and linting especially polydiv
Kazuhiko Sakaguchi
2019-11-27
Explicit `bigop` enumeration handling
Georges Gonthier
2019-11-22
New generalised induction idiom (#434)
Georges Gonthier
2019-09-30
ffact as a product similar to fact_prod (#374)
Laurent Théry
2019-09-16
fermat little theorem
thery
2019-05-08
suppress use of `Arith` hints
Sora Chen
2019-04-26
Cleaning Require and Require Imports
Cyril Cohen
2019-04-01
Making {fun ...} structural and extending it to dependent functions
Georges Gonthier
2019-03-24
Compat of sumn with bigop and renaming dep to cond when appropriate
Cyril Cohen
2018-02-06
running semi-automated linting on the whole library
Cyril Cohen
2018-02-05
tide up proof of card_inj_ffuns
Enrico Tassi
2016-11-07
update copyright banner
Assia Mahboubi
2016-09-16
Refactoring of binonial
thery
2015-11-05
merge basic/ into ssreflect/
Enrico Tassi