diff options
| author | Enrico Tassi | 2020-11-16 21:02:36 +0100 |
|---|---|---|
| committer | GitHub | 2020-11-16 21:02:36 +0100 |
| commit | 068284d23c4a05c7ffeb4db8e277d24ed561369f (patch) | |
| tree | 11817e7ec748ea94296799c0c9817ead9f3890ad /CHANGELOG_UNRELEASED.md | |
| parent | bae9cdb2a12083b8170c3999886839cc1495f969 (diff) | |
| parent | a52c2ba1ff392d3160875e563f28a3d094011111 (diff) | |
Merge pull request #586 from CohenCyril/maxrank
Maximal rank and full rank row submatrices
Diffstat (limited to 'CHANGELOG_UNRELEASED.md')
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index f6f8eca..dbe49c7 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -279,6 +279,13 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). `subseq_rev`, `subseq_cat2l`, `subseq_cat2r`, `subseq_rot`, and `uniq_subseq_pivot`. +- in `mxalgebra.v`, new definitions `maxrankfun`, `fullrankfun` which + are "subset function" to be plugged in `rowsub`, with lemmas: + `maxrowsub_free`, `eq_maxrowsub`, `maxrankfun_inj`, + `maxrowsub_full`, `fullrowsub_full`, `fullrowsub_unit`, + `fullrowsub_free`, `mxrank_fullrowsub`, `eq_fullrowsub`, and + `fullrankfun_inj`. + ### Changed - in `ssrbool.v`, use `Reserved Notation` for `[rel _ _ : _ | _]` to avoid warnings with coq-8.12 |