diff -r a037f01aedab -r 1bd3463e30b8 src/HOL/Analysis/Cartesian_Space.thy
--- a/src/HOL/Analysis/Cartesian_Space.thy	Fri May 07 16:49:08 2021 +0200
+++ b/src/HOL/Analysis/Cartesian_Space.thy	Sun May 09 05:48:50 2021 +0000
@@ -10,7 +10,9 @@
 
 theory Cartesian_Space
   imports
-    Finite_Cartesian_Product Linear_Algebra "HOL-Combinatorics.Transposition"
+    "HOL-Combinatorics.Transposition"
+    Finite_Cartesian_Product
+    Linear_Algebra
 begin
 
 subsection\<^marker>\<open>tag unimportant\<close> \<open>Type @{typ \<open>'a ^ 'n\<close>} and fields as vector spaces\<close> (*much of the following
@@ -1061,7 +1063,7 @@
   then obtain f0 where "bij_betw f0 (UNIV::'n set) S"
     by (metis finite_class.finite_UNIV finite_same_card_bij finiteI_independent)
   then obtain f where f: "bij_betw f (UNIV::'n set) S" and a: "a = f k"
-    using bij_swap_iff [of k "inv f0 a" f0]
+    using bij_swap_iff [of f0 k "inv f0 a"]
     by (metis UNIV_I \<open>a \<in> S\<close> bij_betw_inv_into_right bij_betw_swap_iff swap_apply(1))
   show thesis
   proof
@@ -1206,7 +1208,7 @@
   fixes P :: "real^'n^'n \<Rightarrow> bool"
   assumes zero_row: "\<And>A i. row i A = 0 \<Longrightarrow> P A"
     and diagonal: "\<And>A. (\<And>i j. i \<noteq> j \<Longrightarrow> A$i$j = 0) \<Longrightarrow> P A"
-    and swap_cols: "\<And>A m n. \<lbrakk>P A; m \<noteq> n\<rbrakk> \<Longrightarrow> P(\<chi> i j. A $ i $ Fun.swap m n id j)"
+    and swap_cols: "\<And>A m n. \<lbrakk>P A; m \<noteq> n\<rbrakk> \<Longrightarrow> P(\<chi> i j. A $ i $ Transposition.transpose m n j)"
     and row_op: "\<And>A m n c. \<lbrakk>P A; m \<noteq> n\<rbrakk>
                    \<Longrightarrow> P(\<chi> i. if i = m then row m A + c *\<^sub>R row n A else row i A)"
   shows "P A"
@@ -1293,14 +1295,14 @@
             by blast
         next
           case False
-          have *: "A $ i $ Fun.swap k l id j = 0" if "j \<noteq> k" "j \<notin> K" "i \<noteq> j" for i j
+          have *: "A $ i $ Transposition.transpose k l j = 0" if "j \<noteq> k" "j \<notin> K" "i \<noteq> j" for i j
             using False l insert.prems that
-            by (auto simp: swap_id_eq insert split: if_split_asm)
-          have "P (\<chi> i j. (\<chi> i j. A $ i $ Fun.swap k l id j) $ i $ Fun.swap k l id j)"
+            by (auto simp add: Transposition.transpose_def)
+          have "P (\<chi> i j. (\<chi> i j. A $ i $ Transposition.transpose k l j) $ i $ Transposition.transpose k l j)"
             by (rule swap_cols [OF nonzero_hyp False]) (auto simp: l *)
           moreover
-          have "(\<chi> i j. (\<chi> i j. A $ i $ Fun.swap k l id j) $ i $ Fun.swap k l id j) = A"
-            by (vector Fun.swap_def)
+          have "(\<chi> i j. (\<chi> i j. A $ i $ Transposition.transpose k l j) $ i $ Transposition.transpose k l j) = A"
+            by simp
           ultimately show ?thesis
             by simp
         qed
@@ -1316,14 +1318,14 @@
   assumes mult: "\<And>A B. \<lbrakk>P A; P B\<rbrakk> \<Longrightarrow> P(A ** B)"
     and zero_row: "\<And>A i. row i A = 0 \<Longrightarrow> P A"
     and diagonal: "\<And>A. (\<And>i j. i \<noteq> j \<Longrightarrow> A$i$j = 0) \<Longrightarrow> P A"
-    and swap1: "\<And>m n. m \<noteq> n \<Longrightarrow> P(\<chi> i j. mat 1 $ i $ Fun.swap m n id j)"
+    and swap1: "\<And>m n. m \<noteq> n \<Longrightarrow> P(\<chi> i j. mat 1 $ i $ Transposition.transpose m n j)"
     and idplus: "\<And>m n c. m \<noteq> n \<Longrightarrow> P(\<chi> i j. if i = m \<and> j = n then c else of_bool (i = j))"
   shows "P A"
 proof -
-  have swap: "P (\<chi> i j. A $ i $ Fun.swap m n id j)"  (is "P ?C")
+  have swap: "P (\<chi> i j. A $ i $ Transposition.transpose m n j)"  (is "P ?C")
     if "P A" "m \<noteq> n" for A m n
   proof -
-    have "A ** (\<chi> i j. mat 1 $ i $ Fun.swap m n id j) = ?C"
+    have "A ** (\<chi> i j. mat 1 $ i $ Transposition.transpose m n j) = ?C"
       by (simp add: matrix_matrix_mult_def mat_def vec_eq_iff if_distrib sum.delta_remove)
     then show ?thesis
       using mult swap1 that by metis
@@ -1347,7 +1349,7 @@
   assumes mult: "\<And>A B. \<lbrakk>P A; P B\<rbrakk> \<Longrightarrow> P(A ** B)"
     and zero_row: "\<And>A i. row i A = 0 \<Longrightarrow> P A"
     and diagonal: "\<And>A. (\<And>i j. i \<noteq> j \<Longrightarrow> A$i$j = 0) \<Longrightarrow> P A"
-    and swap1: "\<And>m n. m \<noteq> n \<Longrightarrow> P(\<chi> i j. mat 1 $ i $ Fun.swap m n id j)"
+    and swap1: "\<And>m n. m \<noteq> n \<Longrightarrow> P(\<chi> i j. mat 1 $ i $ Transposition.transpose m n j)"
     and idplus: "\<And>m n. m \<noteq> n \<Longrightarrow> P(\<chi> i j. of_bool (i = m \<and> j = n \<or> i = j))"
   shows "P A"
 proof -
@@ -1386,7 +1388,7 @@
     and comp: "\<And>f g. \<lbrakk>linear f; linear g; P f; P g\<rbrakk> \<Longrightarrow> P(f \<circ> g)"
     and zeroes: "\<And>f i. \<lbrakk>linear f; \<And>x. (f x) $ i = 0\<rbrakk> \<Longrightarrow> P f"
     and const: "\<And>c. P(\<lambda>x. \<chi> i. c i * x$i)"
-    and swap: "\<And>m n::'n. m \<noteq> n \<Longrightarrow> P(\<lambda>x. \<chi> i. x $ Fun.swap m n id i)"
+    and swap: "\<And>m n::'n. m \<noteq> n \<Longrightarrow> P(\<lambda>x. \<chi> i. x $ Transposition.transpose m n i)"
     and idplus: "\<And>m n::'n. m \<noteq> n \<Longrightarrow> P(\<lambda>x. \<chi> i. if i = m then x$m + x$n else x$i)"
   shows "P f"
 proof -
@@ -1415,13 +1417,13 @@
   next
     fix m n :: "'n"
     assume "m \<noteq> n"
-    have eq: "(\<Sum>j\<in>UNIV. if i = Fun.swap m n id j then x $ j else 0) =
-              (\<Sum>j\<in>UNIV. if j = Fun.swap m n id i then x $ j else 0)"
+    have eq: "(\<Sum>j\<in>UNIV. if i = Transposition.transpose m n j then x $ j else 0) =
+              (\<Sum>j\<in>UNIV. if j = Transposition.transpose m n i then x $ j else 0)"
       for i and x :: "real^'n"
       by (rule sum.cong) (auto simp add: swap_id_eq)
-    have "(\<lambda>x::real^'n. \<chi> i. x $ Fun.swap m n id i) = ((*v) (\<chi> i j. if i = Fun.swap m n id j then 1 else 0))"
+    have "(\<lambda>x::real^'n. \<chi> i. x $ Transposition.transpose m n i) = ((*v) (\<chi> i j. if i = Transposition.transpose m n j then 1 else 0))"
       by (auto simp: mat_def matrix_vector_mult_def eq if_distrib [of "\<lambda>x. x * y" for y] cong: if_cong)
-    with swap [OF \<open>m \<noteq> n\<close>] show "P ((*v) (\<chi> i j. mat 1 $ i $ Fun.swap m n id j))"
+    with swap [OF \<open>m \<noteq> n\<close>] show "P ((*v) (\<chi> i j. mat 1 $ i $ Transposition.transpose m n j))"
       by (simp add: mat_def matrix_vector_mult_def)
   next
     fix m n :: "'n"