diff options
Diffstat (limited to 'CHANGELOG_UNRELEASED.md')
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 40 |
1 files changed, 27 insertions, 13 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index ffc1cab..8cb8d9c 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -224,16 +224,20 @@ 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. - - - in `seq.v`, added `in_mask`, `cons_subseq`, `undup_subseq`, `subset_maskP`. - - in `fintype.v`, added `mask_enum_ord`. - - in `bigop.v`, added `big_mask_tuple` and `big_mask`. + 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`, + `count_maskP`, `count_subseqP`, `count_rem`, `count_mem_rem`, + `rem_cons`, `remE`, `subseq_rem`, `leq_uniq_countP`, and + `leq_uniq_count`. +- in `fintype.v`, added `mask_enum_ord`. +- in `bigop.v`, added `big_mask_tuple` and `big_mask`. - in `mxalgebra.v`, new notation `stablemx V f` asserting that `f` stabilizes `V`, with new theorems: `eigenvectorP`, `eqmx_stable`, `stablemx_row_base`, `stablemx_full`, `stablemxM`, `stablemxD`, @@ -271,16 +275,20 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). - in `path.v`, new lemmas `sub_cycle(_in)`, `eq_cycle_in`, `(path|sorted)_(mask|filter)_in`, `rev_cycle`, `cycle_map`, `(homo|mono)_cycle(_in)`. -- in `seq.v` new lemmas `eqseq_pivot`, `rev_mask`, `subseq_rev`, `subseq_cat2l`, `subseq_cat2r`, `subseq_rot`, `subseq_pivot`. -- in `seq.v` new lemmas `eqseq_pivot`, `eqseq_pivot_uniql`, `eqseq_pivot_uniqr`, - `mask_rcons, `rev_mask`, `subseq_rev`, `subseq_cat2l`, `subseq_cat2r`, `subseq_rot`, and - in `seq.v` new lemmas `index_pivot`, `take_pivot`, `rev_pivot`, `eqseq_pivot2l`, `eqseq_pivot2r`, `eqseq_pivotl`, `eqseq_pivotr` `uniq_eqseq_pivotl`, `uniq_eqseq_pivotr`, `mask_rcons`, `rev_mask`, `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 @@ -355,6 +363,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). - in `path.v`, generalized lemmas `sub_path_in`, `sub_sorted_in`, and `eq_path_in` for non-`eqType`s. +- in `order.v`, generalized `sort_le_id` for any `porderType`. + ### Renamed - `big_rmcond` -> `big_rmcond_in` (cf Changed section) @@ -402,6 +412,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). (`allpairs_consr` and `allpairs_catr` are now deprecated alias, and will be attributed to the new `perm_allpairs_catr`). +- in `path.v`, `eq_sorted(_irr)` -> `(irr_)sorted_eq` + - in `div.v` + `coprime_mul(l|r)` -> `coprimeM(l|r)` + `coprime_exp(l|r)` -> `coprimeX(l|r)` @@ -416,6 +428,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). + `primes_(mul|exp)` -> `primes(M|X)` + `pnat_(mul|exp)` -> `pnat(M|X)` +- in `order.v`, `eq_sorted_(le|lt)` -> `(le|lt)_sorted_eq` + - in `ssralg.v` + `prodrMn` has been renamed `prodrMn_const` (with deprecation alias, cf. Added section) |