src/HOL/Analysis/Determinants.thy

   }
   with xe show ?thesis
     by auto
 qed
 
-subsection \<open>Orthogonality of a transformation and matrix.\<close>
+subsection \<open>Orthogonality of a transformation and matrix\<close>
 
 definition "orthogonal_transformation f \<longleftrightarrow> linear f \<and> (\<forall>v w. f v \<bullet> f w = v \<bullet> w)"
 
 lemma orthogonal_transformation:
   "orthogonal_transformation f \<longleftrightarrow> linear f \<and> (\<forall>v. norm (f v) = norm v)"

   fixes f :: "real^'n \<Rightarrow> real^'n"
   shows "orthogonal_transformation f \<Longrightarrow> \<bar>det (matrix f)\<bar> = 1"
   using det_orthogonal_matrix orthogonal_transformation_matrix by fastforce
 
 
-subsection \<open>Linearity of scaling, and hence isometry, that preserves origin.\<close>
+subsection \<open>Linearity of scaling, and hence isometry, that preserves origin\<close>
 
 lemma scaling_linear:
   fixes f :: "'a::real_inner \<Rightarrow> 'a::real_inner"
   assumes f0: "f 0 = 0"
     and fd: "\<forall>x y. dist (f x) (f y) = c * dist x y"

     using assms orthogonal_transformation_surj by blast
   with y assms show "y \<in> f ` cball x r"
     by (auto simp: orthogonal_transformation_isometry)
 qed
 
-subsection\<open> We can find an orthogonal matrix taking any unit vector to any other.\<close>
+subsection\<open> We can find an orthogonal matrix taking any unit vector to any other\<close>
 
 lemma orthogonal_matrix_transpose [simp]:
      "orthogonal_matrix(transpose A) \<longleftrightarrow> orthogonal_matrix A"
   by (auto simp: orthogonal_matrix_def)
 

       using False by auto
   qed (use f in auto)
 qed
 
 
-subsection \<open>Can extend an isometry from unit sphere.\<close>
+subsection \<open>Can extend an isometry from unit sphere\<close>
 
 lemma isometry_sphere_extend:
   fixes f:: "'a::real_inner \<Rightarrow> 'a"
   assumes f1: "\<forall>x. norm x = 1 \<longrightarrow> norm (f x) = 1"
     and fd1: "\<forall> x y. norm x = 1 \<longrightarrow> norm y = 1 \<longrightarrow> dist (f x) (f y) = dist x y"

     using g0 thfg thd
     apply metis
     done
 qed
 
-subsection \<open>Rotation, reflection, rotoinversion.\<close>
+subsection \<open>Rotation, reflection, rotoinversion\<close>
 
 definition "rotation_matrix Q \<longleftrightarrow> orthogonal_matrix Q \<and> det Q = 1"
 definition "rotoinversion_matrix Q \<longleftrightarrow> orthogonal_matrix Q \<and> det Q = - 1"
 
 lemma orthogonal_rotation_or_rotoinversion: