aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/ssreflect
AgeCommit message (Collapse)Author
2020-10-29Switch from long suffixes to short suffixesKazuhiko Sakaguchi
2020-10-12Fixing and documenting the change of meaning of `>=< y`Cyril Cohen
2020-10-12Reorganizing relation between comparability/real and bigCyril Cohen
2020-10-12comparable_big lemma in order.vReynald Affeldt
2020-10-10generalization and shorter proofsCyril Cohen
Co-authored-by: Kazuhiko Sakaguchi <pi8027@gmail.com>
2020-10-09Added results about `mask` and `subseq`Cyril Cohen
2020-10-07Turn class_of records into primitive records and get rid of the xclass idiomKazuhiko Sakaguchi
2020-09-29ssrnat: add subnA, addnCB, addnCAC, addnAl lemmasAnton Trunov
2020-09-29new mem_imset lemmasChristian Doczkal
2020-09-29rename mem_imset2 to imset2_f (with deprecation)Christian Doczkal
2020-09-29rename mem_imset to imset_f (with deprecation)Christian Doczkal
2020-09-28Submatrix theoryCyril Cohen
2020-09-28Merge pull request #555 from chdoc/disjoint-lemmasCyril Cohen
some lemmas for disjoint
2020-09-28Apply suggestions from code reviewKazuhiko Sakaguchi
Co-authored-by: Cyril Cohen <CohenCyril@users.noreply.github.com>
2020-09-27some lemmas for disjointChristian Doczkal
2020-09-27Putting ord1 in fintypeCyril Cohen
ord1 is in zmodp, but it does not really require the zmodType structure of 'I_n to be stated and proven if we state it with ord0. We still keep the variant in zmodp with 0 instead of ord0 (for readability purposes).
2020-09-17Fix big meet and join notations for dual_display, and add `0^d` and `1^d` ↵Kazuhiko Sakaguchi
notations
2020-09-16add missing contra lemmas (fixes #587)Christian Doczkal
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-08split_find_nth and split_find lemmasCyril 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-03compat Coq < 8.10Cyril Cohen
2020-09-03Lemmas reindex_omap and bigD1_ordCyril Cohen
+ eq_liftF and lift_eqF + proof simplificaions
2020-09-03Merge pull request #558 from CohenCyril/are_allpairsEnrico Tassi
Adding allrel predicate
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-03Expliciting relation between split and [lr]shiftCyril 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-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-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-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 #542 from chdoc/nothing-to-injectCyril Cohen
fix "Nothing to inject" warnings
2020-06-26fix "Nothing to inject" warningsChristian Doczkal
2020-06-26lemmas for proper and setCChristian Doczkal
2020-06-24Merge pull request #540 from thery/docCyril Cohen
fix the doc for ubnP in ssrnat
2020-06-24fix the doc for ubnP in ssrnatthery
2020-06-24simpler proofthery
2020-06-18conform to 80 chars limitChristian Doczkal
2020-06-18fixup spacingCyril Cohen
2020-06-18Apply suggestions from code reviewChristian Doczkal
Co-authored-by: Cyril Cohen <CohenCyril@users.noreply.github.com>
2020-06-18drop_uniq / CHANGELOGChristian Doczkal
2020-06-18add fcard_gt?P lemmas found in fourcolorChristian Doczkal
2020-06-18cards_eqP and cards2PChristian Doczkal
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-18 19:20:55 +0000