aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-10-25More arithmetic theoremsCyril Cohen
In ssrnat: - some trivial results in ssrnat `addnKC`, `ltn_predl`, `ltn_predr`, `ltn_subr` and `predn_sub` - theorems about `n <=/< p +/- m` and `m +/- n <=/< p` `leq_psubRL`, `ltn_psubLR`, `leq_subRL`, `ltn_subLR`, `leq_subCl`, `leq_psubCr`, `leq_subCr`, `ltn_subCr`, `ltn_psubCl` and `ltn_subCl` In div: - theorems about the euclidean division of additions and subtraction, + without preconditions of divisibility: `edivnD`, `edivnB`, `divnD`, `divnB`, `modnD`, `modnB` + with divisibility of one argument: `divnDMl`, `divnMBl`, `divnBMl`, `divnBl` and `divnBr` + specialization of the former theorems for .+1 and .-1: `edivnS`, `divnS`, `modnS`, `edivn_pred`, `divn_pred` and `modn_pred`
2019-10-24Added and generalized arithmetic theorems. (#394)Cyril Cohen
- Added: `modn_divl` and `divn_modl`. - Generalized `muln_modr` and `muln_modl` removing hypothesis `0 < p`.
2019-10-21Merge pull request #365 from math-comp/ghpages-redirectMaxime Dénès
Redirects to math-comp.github.io
2019-10-18Add build for mathcomp/mathcomp-dev:coq-8.10 (#391)Erik Martin-Dorel
* feat: Add build for mathcomp/mathcomp-dev:coq-8.10 * fix(coq-mathcomp-ssreflect.opam): Bump coq upper bound * fix(*.opam): Remove "remove" directive href: coq/opam-coq-archive#703
2019-10-16Merge pull request #203 from CohenCyril/improving_fintype_bigopMaxime Dénès
Improving fintype and bigop
2019-10-16shifting to CHANGELOG_UNRELEASEDCyril Cohen
2019-10-16renaming new `reindex_` lemmas with prefix `big_`Cyril Cohen
2019-10-16Improving fintype and bigopCyril Cohen
### Added - Fintype theorems: `fintype0`, `card_le1P`, `mem_card1`, `card1P`, `fintype_le1P`, `fintype1`, `fintype1P`. - Bigop theorems: `big_rmcond`, `bigD1_seq`, `reindex_enum_val_cond`, `reindex_enum_rank_cond`, `reindex_enum_val`, `reindex_enum_rank`, `big_set`.
2019-10-16removing everything but index which redirects to the new pageCyril Cohen
2019-10-15Merge pull request #390 from thery/docCyril Cohen
typo in ssralg
2019-10-14typothery
2019-10-07Merge pull request #384 from pi8027/hierarchyCyril Cohen
Fix and improve the test suite and Makefile
2019-10-07Merge pull request #387 from pi8027/seq-lemmasCyril Cohen
Add `flatten_map1` and `allpairs_consr`
2019-10-05Add flatten_map1 and allpairs_consrKazuhiko Sakaguchi
2019-10-02Fix and improve the test suite and MakefileKazuhiko Sakaguchi
- improve an error message produced by the `check_join` tactic, - fix the build of the test suite: `make test-suite`, and - add a new rule `only` to build a subset of MathComp.
2019-10-01Merge pull request #386 from pi8027/allpairsCyril Cohen
Generalize `allpairs_catr` to non-`eqType`s
2019-09-30Generalize `allpairs_catr` to non-`eqType`sKazuhiko Sakaguchi
2019-09-30Euclid theorem for product (#375)Laurent Théry
2019-09-30ffact as a product similar to fact_prod (#374)Laurent Théry
Thanks!
2019-09-28maxn comment fix (#385)Antonio Nikishaev
2019-09-24Merge pull request #380 from pi8027/ring-core-scopeCyril Cohen
Fix a typo: `ring_core_scope`
2019-09-18Fix a typo: ring_core_scope -> ring_scopeKazuhiko Sakaguchi
2019-09-16fermat little theoremthery
2019-09-05Redirects to math-comp.github.ioCyril Cohen
Merge only after solving issue https://github.com/math-comp/math-comp/issues/361
2019-08-12Merge pull request #376 from erikmd/fix-gitlab-yamlCyril Cohen
[ci] fix .gitlab-ci.yml regarding "GIT_STRATEGY: none"
2019-08-10fix(.gitlab-ci.yml): duplicated "variables:" entryErik Martin-Dorel
This could explain why the change in b8eadb8603b83c053a313b39c2a8f268385d8942 was not taken into account.
2019-08-02Merge pull request #373 from erikmd/improve-ciCyril Cohen
[ci] a few improvements of the GitLab CI setup
2019-07-30[ci] Adapt the GitLab CI config to allow scheduled builds for coq-devErik Martin-Dorel
* Normal builds (branches & GitHub PRs) are not impacted * Triggering a scheduled pipeline will only run {coq-dev, mathcomp-dev:coq-dev} to build and deploy the corresponding image to mathcomp/mathcomp-dev:coq-dev. * href: https://docs.gitlab.com/ce/user/project/pipelines/schedules.html
2019-07-30[ci] Add jobs {ci-fourcolor-8.9, ci-odd-order-8.9}Erik Martin-Dorel
* Add {fourcolor, odd-order} test builds with latest Coq release (8.9) * As a result, the math-comp CI config w.r.t. {fourcolor, odd-order} will be similar to that of the upstream repos: - https://github.com/math-comp/fourcolor/blob/master/.travis.yml - https://github.com/math-comp/odd-order/pull/16
2019-07-30refactor: deploy jobs need not clone the repoErik Martin-Dorel
* Set "GIT_STRATEGY: none" accordingly
2019-07-29style: fix indentation detailErik Martin-Dorel
2019-07-11Merge pull request #369 from thery/totientCyril Cohen
totient for prime
2019-07-10totient for primethery
2019-07-05feat(finfun.v): Add tuple_of_finfun, finfun_of_tuple & cancel lemmasCyril Cohen
2019-06-26Merge pull request #364 from erikmd/update/changelogCyril Cohen
docs: Add missing entry in CHANGELOG.md regarding #292
2019-06-26docs: Add missing entry in CHANGELOG.mdErik Martin-Dorel
href: math-comp/math-comp#292
2019-06-18Merge pull request #340 from pi8027/hierarchyEnrico
Reimplement the hierarchy related tools in OCaml
2019-06-11Merge pull request #302 from CohenCyril/fixsetGeorges Gonthier
Fixpoint theorems in finset
2019-06-04Fixpoint theorems in finsetCyril Cohen
2019-05-29Merge pull request #353 from anton-trunov/update-ciCyril Cohen
Remove support for Travis CI (mathcomp switched to Gitlab CI)
2019-05-29Replace eqVneq to destruct both x == y, but also y == x (#351)Cyril Cohen
2019-05-29Remove support for Travis CIAnton Trunov
Mathcomp switched to Gitlab CI via coqbot, see here: https://github.com/math-comp/math-comp/pull/353#issuecomment-497017174
2019-05-29Update pull_request_template.mdCyril Cohen
2019-05-29Merge pull request #352 from CohenCyril/pr_tempateCyril Cohen
PR template
2019-05-29reword entry in CHANGELOG_UNRELEASED.mdAnton Trunov
2019-05-29Update pull_request_template.mdCyril Cohen
2019-05-29Move unreleased changelog entries to CHANGELOG_UNRELEASED.mdAnton Trunov
2019-05-29pr templateCyril Cohen
2019-05-29incorporate new suggestions by @CohenCyrilAnton Trunov
2019-05-29Replace eqVneq with eqPsymAnton Trunov
Also changed eqsVneq.
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 11:04:23 +0000