diff options
| author | Laurent Théry | 2020-11-16 16:54:53 +0100 |
|---|---|---|
| committer | GitHub | 2020-11-16 16:54:53 +0100 |
| commit | bae9cdb2a12083b8170c3999886839cc1495f969 (patch) | |
| tree | 9d33feef64df064a0fecd6222b6c656072fbaa95 /CHANGELOG_UNRELEASED.md | |
| parent | 1a098263b335ccc4cf72880662dccbe79185a8ab (diff) | |
| parent | 8b98bcedc4523e07e4fdc118159cf171366e952d (diff) | |
Merge pull request #636 from CohenCyril/fix_comm_mxC
`comm(Cmx|_mxC)` -> `comm(_scalar_mx|_mx_scalar)`
Diffstat (limited to 'CHANGELOG_UNRELEASED.md')
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 68eb6d5..f6f8eca 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -221,12 +221,12 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). boolean versions of matrix commutation, `comm_mx A B` is definitionally equal to `GRing.comm A B` when `A B : 'M_n.+1`, this is witnessed by the lemma `comm_mxE`. New notation `all_comm_mx` - stands for `allrel comm_mxb`. New lemmas `comm_mx_sym`, `comm_mx_refl`, - `comm_mx0`, `comm0mx`, `comm_mx1`, `comm1mx`, `comm_mxN`, `comm_mxN1`, - `comm_mxD`, `comm_mxB`, `comm_mx_sum`, `comm_mxP`, `all_comm_mxP`, - `all_comm_mx1`, `all_comm_mx2P`, `all_comm_mx_cons`, `comm_mxC`, and - `commCmx`. The common arguments of these lemmas `R` and `n` are - maximal implicits. + stands for `allrel comm_mxb`. New lemmas `comm_mx_sym`, + `comm_mx_refl`, `comm_mx0`, `comm0mx`, `comm_mx1`, `comm1mx`, + `comm_mxN`, `comm_mxN1`, `comm_mxD`, `comm_mxB`, `comm_mx_sum`, + `comm_mxP`, `all_comm_mxP`, `all_comm_mx1`, `all_comm_mx2P`, + `all_comm_mx_cons`, `comm_mx_scalar`, and `comm_scalar_mx`. The + common arguments of these lemmas `R` and `n` are maximal implicits. - in `seq.v`, added `drop_index`, `in_mask`, `cons_subseq`, `undup_subseq`, `leq_count_mask`, `leq_count_subseq`, |