Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Combinatorics/Transposition.thy
changeset 82683 71304514891e
parent 73664 6e26d06b24b1 
--- a/src/HOL/Combinatorics/Transposition.thy	Sun Jun 01 20:01:22 2025 +0200
+++ b/src/HOL/Combinatorics/Transposition.thy	Tue Jun 03 12:22:58 2025 +0200
@@ -10,7 +10,7 @@
 lemma transpose_apply_first [simp]:
   \<open>transpose a b a = b\<close>
   by (simp add: transpose_def)
-
+                           
 lemma transpose_apply_second [simp]:
   \<open>transpose a b b = a\<close>
   by (simp add: transpose_def)
@@ -43,6 +43,9 @@
   \<open>transpose a b \<circ> transpose a b = id\<close>
   by (rule ext) simp
 
+lemma transpose_eq_id_iff: "Transposition.transpose x y = id \<longleftrightarrow> x = y"
+  by (auto simp: fun_eq_iff Transposition.transpose_def)
+
 lemma transpose_triple:
   \<open>transpose a b (transpose b c (transpose a b d)) = transpose a c d\<close>
   if \<open>a \<noteq> c\<close> and \<open>b \<noteq> c\<close>
isabelle