diff -r 06aac7eaec29 -r 71304514891e src/HOL/Combinatorics/Transposition.thy
--- 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>