diff options
| author | Cyril Cohen | 2020-11-09 01:06:18 +0100 |
|---|---|---|
| committer | Cyril Cohen | 2020-11-09 01:06:18 +0100 |
| commit | 8b98bcedc4523e07e4fdc118159cf171366e952d (patch) | |
| tree | aa5fd79fd3938e2e529dd1142e77ecab283af244 /CHANGELOG_UNRELEASED.md | |
| parent | c33309d4279c5d6483af54b54fe6aa326e289f9b (diff) | |
`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 57e5e28..e78d37d 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 `in_mask`, `cons_subseq`, `undup_subseq`, `subset_maskP`. - in `fintype.v`, added `mask_enum_ord`. |