src/HOL/Analysis/Linear_Algebra.thy
changeset 69683 8b3458ca0762
parent 69675 880ab0f27ddf
child 70136 f03a01a18c6e
     1.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Thu Jan 17 16:37:06 2019 -0500
     1.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Thu Jan 17 16:38:00 2019 -0500
     1.3 @@ -297,7 +297,7 @@
     1.4  qed
     1.5  
     1.6  
     1.7 -subsection%important  \<open>Orthogonality of a transformation\<close>
     1.8 +subsection  \<open>Orthogonality of a transformation\<close>
     1.9  
    1.10  definition%important  "orthogonal_transformation f \<longleftrightarrow> linear f \<and> (\<forall>v w. f v \<bullet> f w = v \<bullet> w)"
    1.11