src/HOL/Analysis/Cartesian_Euclidean_Space.thy

   show "x v* (k *\<^sub>R A) = k *\<^sub>R (x v* A)"
     by auto
 qed
 
 
-subsection%important\<open>Some bounds on components etc. relative to operator norm\<close>
+subsection%important\<open>Bounds on components etc.\ relative to operator norm\<close>
 
 lemma%important norm_column_le_onorm:
   fixes A :: "real^'n^'m"
   shows "norm(column i A) \<le> onorm((*v) A)"
 proof%unimportant -