Add a theory of finite permutations.

arthuraa · CohenCyril · commit 4672b5487c78 · 2026-02-27T23:40:21.000+01:00
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -7,6 +7,8 @@
 - in `finmap.v`:
   + lemma `card_fset_sum1`
 
+- Added a theory of finite permutations in `finperm.v`
+
 ### Changed
 
 ### Renamed
diff --git a/_CoqProject b/_CoqProject
@@ -1,5 +1,6 @@
 finmap.v
 multiset.v
+finperm.v
 
 -R . mathcomp.finmap
 -arg -w -arg -projection-no-head-constant
diff --git a/finperm.v b/finperm.v
