| changeset 64122 | 74fde524799e |
| parent 63938 | f6ce08859d4c |
| child 64267 | b9a1486e79be |
--- a/src/HOL/Analysis/Linear_Algebra.thy Sun Oct 09 16:27:01 2016 +0200 +++ b/src/HOL/Analysis/Linear_Algebra.thy Mon Oct 10 15:45:41 2016 +0100 @@ -2178,7 +2178,7 @@ text \<open>More lemmas about dimension.\<close> -lemma dim_UNIV: "dim (UNIV :: 'a::euclidean_space set) = DIM('a)" +lemma dim_UNIV [simp]: "dim (UNIV :: 'a::euclidean_space set) = DIM('a)" using independent_Basis by (intro dim_unique[of Basis]) auto