diff -r 4dc3baf45d6a -r 5020054b3a16 src/HOL/Analysis/Cartesian_Space.thy
--- a/src/HOL/Analysis/Cartesian_Space.thy	Wed May 05 16:09:02 2021 +0000
+++ b/src/HOL/Analysis/Cartesian_Space.thy	Wed May 05 16:09:02 2021 +0000
@@ -10,7 +10,7 @@
 
 theory Cartesian_Space
   imports
-    Finite_Cartesian_Product Linear_Algebra
+    Finite_Cartesian_Product Linear_Algebra "HOL-Combinatorics.Transposition"
 begin
 
 subsection\<^marker>\<open>tag unimportant\<close> \<open>Type @{typ \<open>'a ^ 'n\<close>} and fields as vector spaces\<close> (*much of the following