aboutsummaryrefslogtreecommitdiff
path: root/mathcomp
AgeCommit message (Collapse)Author
2020-09-10Update mathcomp/Makefile.test-suite.coq.localEnrico Tassi
Co-authored-by: Erik Martin-Dorel <erik@martin-dorel.org>
2020-09-10Update mathcomp/Makefile.test-suite.coq.localEnrico Tassi
Co-authored-by: Erik Martin-Dorel <erik@martin-dorel.org>
2020-09-10Merge pull request #492 from CohenCyril/big_rmcondKazuhiko Sakaguchi
New `big_uncond` and `big_rmcond -> big_rmcond_in`
2020-09-10Merge pull request #578 from CohenCyril/contra_leKazuhiko Sakaguchi
Adding contra lemmas with orders
2020-09-09default reference file for < 8.12Enrico Tassi
2020-09-08Adding sub_sums_genmxP (generalizes sub_sumsmxP)Cyril Cohen
2020-09-08Merge pull request #573 from CohenCyril/horner_diagLaurent Théry
Polynomial evaluation and minimal/char poly of a diagonal/triangular matrices
2020-09-08Merge pull request #577 from CohenCyril/mulmxPaffeldt-aist
Lemma mul_rVP
2020-09-08Lemma mul_rvPCyril Cohen
2020-09-08split_find_nth and split_find lemmasCyril Cohen
2020-09-07Adding [row|col]_[udlr]submx lemmasCyril Cohen
2020-09-07[test suite] infrastructure to test how some statements are printedEnrico Tassi
2020-09-07compat Coq < 8.10Cyril Cohen
2020-09-07Refactoring proof of det_trig and spawning sublemmasCyril Cohen
2020-09-07Polynomial evaluation and minimal poly of a diagonal matrixCyril Cohen
2020-09-05Adding contra lemmas with ordersCyril Cohen
- Adding contra lemmas between `leq`, `ltn`, `Order.le` ("le"), `Order.lt` ("lt"), `b` ("T"), `~~ b` ("N"), `b = false` ("F"), and `~ P` ("not"). - Changelog for contra lemmas with orders Co-authored-by: Reynald Affeldt <reynald.affeldt@aist.go.jp>
2020-09-04Adding more map_mx lemmasCyril Cohen
2020-09-04Merge pull request #575 from CohenCyril/mxOverLaurent Théry
Adding mxOver predicate
2020-09-03compat Coq < 8.10Cyril Cohen
2020-09-03Lemmas reindex_omap and bigD1_ordCyril Cohen
+ eq_liftF and lift_eqF + proof simplificaions
2020-09-03Merge branch 'missing_mxalgebra' of https://github.com/CohenCyril/math-comp ↵thery
into CohenCyril-missing_mxalgebra
2020-09-03Lemmas mxminpoly_minP and dvd_mxminpolyCyril Cohen
2020-09-03Adding missing mxalgebra lemmasCyril Cohen
2020-09-03Merge pull request #558 from CohenCyril/are_allpairsEnrico Tassi
Adding allrel predicate
2020-09-03Merge pull request #565 from CohenCyril/split_ordPLaurent Théry
Expliciting relation between split and [lr]shift
2020-09-03Merge pull request #564 from CohenCyril/pinvmxLaurent Théry
More pinvmx theory
2020-09-03Adding allrel predicateCyril Cohen
2020-09-03New `big_uncond` and `big_rmcond -> big_rmcond_in`Cyril Cohen
- Lemma `big_rmcond` has been renamed `big_rmcomd_in` and the variant which does not require an `eqType` has been added and named `big_uncond`. - The name `big_rmcond` is deprecated and will be reused for `big_uncond` in the next version of math-comp - Additionally `big_uncond_in` is made available for uniformity, but is already deprecated.
2020-09-03Merge pull request #560 from CohenCyril/commr_hornerLaurent Théry
Adding commr_horner lemma
2020-09-03More pinvmx theoryCyril Cohen
2020-09-03Adding mxOver predicateCyril Cohen
2020-09-03Adding commr_horner lemmaCyril Cohen
2020-09-03Expliciting relation between split and [lr]shiftCyril Cohen
2020-09-03Extracting a nonzero coefficient from a nonzero matrixCyril Cohen
+ shortening some proofs
2020-09-03Elementary theory of diagonal and triagular matricesCyril Cohen
2020-09-01fix for Coq 8.7Cyril Cohen
2020-09-01Adding sig_big_dep lemmaCyril Cohen
2020-08-25Adding lemma `oddS`Cyril Cohen
2020-08-20Merge pull request #550 from jashug/dont-refresh-argument-names-overlayEnrico Tassi
Be robust to a change in the default argument naming algorithm.
2020-08-17Qualify the dual_* notations with the Order moduleKazuhiko Sakaguchi
2020-08-16Merge pull request #517 from thery/minnCyril Cohen
Extra theorems about subn minn and maxn
2020-08-15Extra theorems about subn min and maxthery
2020-08-13Be robust to a change in the default argument naming algorithm.Jasper Hugunin
Overlay for coq/coq#12756, which changes the default argument name to just `S` from `S0`. This change preserves the old name; switching instead to use `S` may be preferable but introduces a potential impact on downstream users of mathcomp.
2020-08-13Merge pull request #545 from pi8027/fieldextCyril Cohen
Make [fieldExtType F of L] work for abstract instances
2020-08-13Merge pull request #553 from chdoc/non-reversible-notationCyril Cohen
fix non-reversible-notation warnings
2020-08-13fix non-reversible-notation warningsChristian Doczkal
2020-08-12Make [fieldExtType F of L] work for abstract instancesKazuhiko Sakaguchi
2020-08-12Get rid of displays in class fields and mixin parametersKazuhiko Sakaguchi
- In the definition of structures in order.v, displays are removed from parameters of mixins and fields of classes internally and now only appear in parameters of structures. Consequently, each mixin is now parameterized by a class rather than a structure, and the corresponding factory parameterized by a structure is provided to replace the use of the mixin. These factories have the same names as in the mixins before this change except that `bLatticeMixin` and `tbLatticeMixin` have been renamed to `bottomMixin` and `topMixin` respectively. - Added a factory `distrLatticePOrderMixin` in order.v to build a `distrLatticeType` from a `porderType`.
2020-08-11fix notation-incompatible-format warningsChristian Doczkal
2020-08-11Merge pull request #507 from pi8027/test-guard-condCyril Cohen
Add more test cases for higher-order recursive functions in seq.v w.r.t. the guard condition
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 08:16:42 +0000