diff options
| author | Laurent Théry | 2020-09-28 08:41:58 +0200 |
|---|---|---|
| committer | GitHub | 2020-09-28 08:41:58 +0200 |
| commit | a97b433c2d81c702fe690101a6e4e7afb4a3c28d (patch) | |
| tree | 23daffbce553ac1ddfdb22ee9e5d9d4c35937518 /CHANGELOG_UNRELEASED.md | |
| parent | 6d8f919bbc6a103378005d282fb6018bb63c5026 (diff) | |
| parent | 9eb54ad40f57b90d9c3b611a930994f99a46c7ea (diff) | |
Merge pull request #598 from CohenCyril/det_mx11
det_mx11
Diffstat (limited to 'CHANGELOG_UNRELEASED.md')
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 95c0d63..0a59193 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -136,6 +136,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). - in `order.v`, new notations `0^d` and `1^d` for bottom and top elements of dual lattices. +- in `matrix.v` new lemma `det_mx11`. + ### Changed - in ssrbool.v, use `Reserved Notation` for `[rel _ _ : _ | _]` to avoid warnings with coq-8.12 |