diff options
| author | Anton Trunov | 2020-04-01 19:52:45 +0300 |
|---|---|---|
| committer | GitHub | 2020-04-01 19:52:45 +0300 |
| commit | ca8cd06caa1bd11aa33bd01b2fcd79893d4df800 (patch) | |
| tree | 49bb3ca6df5e6117d9f4b506fe8b2feeaf452c72 /doc | |
| parent | b4524a7e8deb0144cb00ee2db823c98392fb208e (diff) | |
| parent | f6b0f54f4f7671f37c6ab991753d4045590355bf (diff) | |
Merge pull request #11946 from olaure01/ollibs-permutation
[stdlib] Add complementary results about Permutation
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/10-standard-library/11946-ollibs-permutation.rst | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/doc/changelog/10-standard-library/11946-ollibs-permutation.rst b/doc/changelog/10-standard-library/11946-ollibs-permutation.rst new file mode 100644 index 0000000000..626677d31a --- /dev/null +++ b/doc/changelog/10-standard-library/11946-ollibs-permutation.rst @@ -0,0 +1,10 @@ +- **Added:** + Facts about ``Permutation``: + + - structure: ``Permutation_refl'``, ``Permutation_morph_transp`` + - compatibilities: ``Permutation_app_rot``, ``Permutation_app_swap_app``, ``Permutation_app_middle``, ``Permutation_middle2``, ``Permutation_elt``, ``Permutation_Forall``, ``Permutation_Exists``, ``Permutation_Forall2``, ``Permutation_flat_map``, ``Permutation_list_sum``, ``Permutation_list_max`` + - inversions: ``Permutation_app_inv_m``, ``Permutation_vs_elt_inv``, ``Permutation_vs_cons_inv``, ``Permutation_vs_cons_cons_inv``, ``Permutation_map_inv``, ``Permutation_image``, ``Permutation_elt_map_inv`` + - length-preserving definition by means of transpositions ``Permutation_transp`` with associated properties: ``Permutation_transp_sym``, ``Permutation_transp_equiv``, ``Permutation_transp_cons``, ``Permutation_Permutation_transp``, ``Permutation_ind_transp`` + + (`#11946 <https://github.com/coq/coq/pull/11946>`_, + by Olivier Laurent). |