| changeset 73623 | 5020054b3a16 |
| parent 73466 | ee1c4962671c |
| child 73648 | 1bd3463e30b8 |
--- 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