src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy

   by (simp add: basis_eq_0)
 
 text {* some lemmas to map between Eucl and Cart *}
 lemma basis_real_n[simp]:"(basis (\<pi>' i)::real^'a) = cart_basis i"
   unfolding basis_vec_def using pi'_range[where 'n='a]
-  by (auto simp: vec_eq_iff)
+  by (auto simp: vec_eq_iff axis_def)
 
 subsection {* Orthogonality on cartesian products *}
 
 lemma orthogonal_basis:
   shows "orthogonal (cart_basis i) x \<longleftrightarrow> x$i = (0::real)"