--- a/src/HOL/Analysis/Euclidean_Space.thy Sun May 27 22:57:06 2018 +0100
+++ b/src/HOL/Analysis/Euclidean_Space.thy Mon May 28 23:15:23 2018 +0100
@@ -253,6 +253,12 @@
lemma DIM_complex[simp]: "DIM(complex) = 2"
unfolding Basis_complex_def by simp
+lemma complex_Basis_1 [iff]: "(1::complex) \<in> Basis"
+ by (simp add: Basis_complex_def)
+
+lemma complex_Basis_i [iff]: "\<i> \<in> Basis"
+ by (simp add: Basis_complex_def)
+
subsubsection%unimportant \<open>Type @{typ "'a \<times> 'b"}\<close>
instantiation%important prod :: (euclidean_space, euclidean_space) euclidean_space