src/HOL/Analysis/Determinants.thy

   "HOL-Library.Permutations"
 begin
 
 subsection  \<open>Trace\<close>
 
-definition%important  trace :: "'a::semiring_1^'n^'n \<Rightarrow> 'a"
+definition\<^marker>\<open>tag important\<close>  trace :: "'a::semiring_1^'n^'n \<Rightarrow> 'a"
   where "trace A = sum (\<lambda>i. ((A$i)$i)) (UNIV::'n set)"
 
 lemma  trace_0: "trace (mat 0) = 0"
   by (simp add: trace_def mat_def)
 

   apply (simp add: trace_def matrix_matrix_mult_def)
   apply (subst sum.swap)
   apply (simp add: mult.commute)
   done
 
-subsubsection%important  \<open>Definition of determinant\<close>
-
-definition%important  det:: "'a::comm_ring_1^'n^'n \<Rightarrow> 'a" where
+subsubsection\<^marker>\<open>tag important\<close>  \<open>Definition of determinant\<close>
+
+definition\<^marker>\<open>tag important\<close>  det:: "'a::comm_ring_1^'n^'n \<Rightarrow> 'a" where
   "det A =
     sum (\<lambda>p. of_int (sign p) * prod (\<lambda>i. A$i$p i) (UNIV :: 'n set))
       {p. p permutes (UNIV :: 'n set)}"
 
 text \<open>Basic determinant properties\<close>

   fixes A :: "real^'n^'n"
   shows "det A = 0 \<longleftrightarrow> rank A < CARD('n)"
   using invertible_det_nz [of A]
   by (auto simp: matrix_left_invertible_injective invertible_left_inverse less_rank_noninjective)
 
-subsubsection%important  \<open>Invertibility of matrices and corresponding linear functions\<close>
+subsubsection\<^marker>\<open>tag important\<close>  \<open>Invertibility of matrices and corresponding linear functions\<close>
 
 lemma  matrix_left_invertible_gen:
   fixes f :: "'a::field^'m \<Rightarrow> 'a::field^'n"
   assumes "Vector_Spaces.linear (*s) (*s) f"
   shows "((\<exists>B. B ** matrix f = mat 1) \<longleftrightarrow> (\<exists>g. Vector_Spaces.linear (*s) (*s) g \<and> g \<circ> f = id))"

 qed
 
 proposition  orthogonal_transformation_det [simp]:
   fixes f :: "real^'n \<Rightarrow> real^'n"
   shows "orthogonal_transformation f \<Longrightarrow> \<bar>det (matrix f)\<bar> = 1"
-  using%unimportant det_orthogonal_matrix orthogonal_transformation_matrix by fastforce
+  using det_orthogonal_matrix orthogonal_transformation_matrix by fastforce
 
 subsection  \<open>Rotation, reflection, rotoinversion\<close>
 
-definition%important  "rotation_matrix Q \<longleftrightarrow> orthogonal_matrix Q \<and> det Q = 1"
-definition%important  "rotoinversion_matrix Q \<longleftrightarrow> orthogonal_matrix Q \<and> det Q = - 1"
+definition\<^marker>\<open>tag important\<close>  "rotation_matrix Q \<longleftrightarrow> orthogonal_matrix Q \<and> det Q = 1"
+definition\<^marker>\<open>tag important\<close>  "rotoinversion_matrix Q \<longleftrightarrow> orthogonal_matrix Q \<and> det Q = - 1"
 
 lemma  orthogonal_rotation_or_rotoinversion:
   fixes Q :: "'a::linordered_idom^'n^'n"
   shows " orthogonal_matrix Q \<longleftrightarrow> rotation_matrix Q \<or> rotoinversion_matrix Q"
   by (metis rotoinversion_matrix_def rotation_matrix_def det_orthogonal_matrix)