src/HOL/Analysis/Determinants.thy

 subsection  \<open>Trace\<close>
 
 definition%important  trace :: "'a::semiring_1^'n^'n \<Rightarrow> 'a"
   where "trace A = sum (\<lambda>i. ((A$i)$i)) (UNIV::'n set)"
 
-lemma%unimportant  trace_0: "trace (mat 0) = 0"
+lemma  trace_0: "trace (mat 0) = 0"
   by (simp add: trace_def mat_def)
 
-lemma%unimportant  trace_I: "trace (mat 1 :: 'a::semiring_1^'n^'n) = of_nat(CARD('n))"
+lemma  trace_I: "trace (mat 1 :: 'a::semiring_1^'n^'n) = of_nat(CARD('n))"
   by (simp add: trace_def mat_def)
 
-lemma%unimportant  trace_add: "trace ((A::'a::comm_semiring_1^'n^'n) + B) = trace A + trace B"
+lemma  trace_add: "trace ((A::'a::comm_semiring_1^'n^'n) + B) = trace A + trace B"
   by (simp add: trace_def sum.distrib)
 
-lemma%unimportant  trace_sub: "trace ((A::'a::comm_ring_1^'n^'n) - B) = trace A - trace B"
+lemma  trace_sub: "trace ((A::'a::comm_ring_1^'n^'n) - B) = trace A - trace B"
   by (simp add: trace_def sum_subtractf)
 
-lemma%important  trace_mul_sym: "trace ((A::'a::comm_semiring_1^'n^'m) ** B) = trace (B**A)"
+lemma  trace_mul_sym: "trace ((A::'a::comm_semiring_1^'n^'m) ** B) = trace (B**A)"
   apply (simp add: trace_def matrix_matrix_mult_def)
   apply (subst sum.swap)
   apply (simp add: mult.commute)
   done
 
-subsubsection  \<open>Definition of determinant\<close>
+subsubsection%important  \<open>Definition of determinant\<close>
 
 definition%important  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>
 
-lemma%important  det_transpose [simp]: "det (transpose A) = det (A::'a::comm_ring_1 ^'n^'n)"
-proof%unimportant -
+lemma  det_transpose [simp]: "det (transpose A) = det (A::'a::comm_ring_1 ^'n^'n)"
+proof -
   let ?di = "\<lambda>A i j. A$i$j"
   let ?U = "(UNIV :: 'n set)"
   have fU: "finite ?U" by simp
   {
     fix p

   then show ?thesis
     unfolding det_def
     by (subst sum_permutations_inverse) (blast intro: sum.cong)
 qed
 
-lemma%unimportant  det_lowerdiagonal:
+lemma  det_lowerdiagonal:
   fixes A :: "'a::comm_ring_1^('n::{finite,wellorder})^('n::{finite,wellorder})"
   assumes ld: "\<And>i j. i < j \<Longrightarrow> A$i$j = 0"
   shows "det A = prod (\<lambda>i. A$i$i) (UNIV:: 'n set)"
 proof -
   let ?U = "UNIV:: 'n set"

   qed
   from sum.mono_neutral_cong_left[OF finite_permutations[OF fU] id0 p0] show ?thesis
     unfolding det_def by (simp add: sign_id)
 qed
 
-lemma%important  det_upperdiagonal:
+lemma  det_upperdiagonal:
   fixes A :: "'a::comm_ring_1^'n::{finite,wellorder}^'n::{finite,wellorder}"
   assumes ld: "\<And>i j. i > j \<Longrightarrow> A$i$j = 0"
   shows "det A = prod (\<lambda>i. A$i$i) (UNIV:: 'n set)"
-proof%unimportant -
+proof -
   let ?U = "UNIV:: 'n set"
   let ?PU = "{p. p permutes ?U}"
   let ?pp = "(\<lambda>p. of_int (sign p) * prod (\<lambda>i. A$i$p i) (UNIV :: 'n set))"
   have fU: "finite ?U"
     by simp

   qed
   from sum.mono_neutral_cong_left[OF finite_permutations[OF fU] id0 p0] show ?thesis
     unfolding det_def by (simp add: sign_id)
 qed
 
-lemma%important  det_diagonal:
+proposition  det_diagonal:
   fixes A :: "'a::comm_ring_1^'n^'n"
   assumes ld: "\<And>i j. i \<noteq> j \<Longrightarrow> A$i$j = 0"
   shows "det A = prod (\<lambda>i. A$i$i) (UNIV::'n set)"
-proof%unimportant -
+proof -
   let ?U = "UNIV:: 'n set"
   let ?PU = "{p. p permutes ?U}"
   let ?pp = "\<lambda>p. of_int (sign p) * prod (\<lambda>i. A$i$p i) (UNIV :: 'n set)"
   have fU: "finite ?U" by simp
   from finite_permutations[OF fU] have fPU: "finite ?PU" .

   qed
   from sum.mono_neutral_cong_left[OF fPU id0 p0] show ?thesis
     unfolding det_def by (simp add: sign_id)
 qed
 
-lemma%unimportant  det_I [simp]: "det (mat 1 :: 'a::comm_ring_1^'n^'n) = 1"
+lemma  det_I [simp]: "det (mat 1 :: 'a::comm_ring_1^'n^'n) = 1"
   by (simp add: det_diagonal mat_def)
 
-lemma%unimportant  det_0 [simp]: "det (mat 0 :: 'a::comm_ring_1^'n^'n) = 0"
+lemma  det_0 [simp]: "det (mat 0 :: 'a::comm_ring_1^'n^'n) = 0"
   by (simp add: det_def prod_zero power_0_left)
 
-lemma%unimportant  det_permute_rows:
+lemma  det_permute_rows:
   fixes A :: "'a::comm_ring_1^'n^'n"
   assumes p: "p permutes (UNIV :: 'n::finite set)"
   shows "det (\<chi> i. A$p i :: 'a^'n^'n) = of_int (sign p) * det A"
 proof -
   let ?U = "UNIV :: 'n set"

     apply (subst sum_permutations_compose_right[OF p])
     apply (rule *)
     done
 qed
 
-lemma%important  det_permute_columns:
+lemma  det_permute_columns:
   fixes A :: "'a::comm_ring_1^'n^'n"
   assumes p: "p permutes (UNIV :: 'n set)"
   shows "det(\<chi> i j. A$i$ p j :: 'a^'n^'n) = of_int (sign p) * det A"
-proof%unimportant -
+proof -
   let ?Ap = "\<chi> i j. A$i$ p j :: 'a^'n^'n"
   let ?At = "transpose A"
   have "of_int (sign p) * det A = det (transpose (\<chi> i. transpose A $ p i))"
     unfolding det_permute_rows[OF p, of ?At] det_transpose ..
   moreover

     by (simp add: transpose_def vec_eq_iff)
   ultimately show ?thesis
     by simp
 qed
 
-lemma%unimportant  det_identical_columns:
+lemma  det_identical_columns:
   fixes A :: "'a::comm_ring_1^'n^'n"
   assumes jk: "j \<noteq> k"
     and r: "column j A = column k A"
   shows "det A = 0"
 proof -

   also have "\<dots>= sum ?f ?S1 - sum ?f ?S1 " unfolding * by auto
   also have "\<dots>= 0" by simp
   finally show "det A = 0" by simp
 qed
 
-lemma%unimportant  det_identical_rows:
+lemma  det_identical_rows:
   fixes A :: "'a::comm_ring_1^'n^'n"
   assumes ij: "i \<noteq> j" and r: "row i A = row j A"
   shows "det A = 0"
   by (metis column_transpose det_identical_columns det_transpose ij r)
 
-lemma%unimportant  det_zero_row:
+lemma  det_zero_row:
   fixes A :: "'a::{idom, ring_char_0}^'n^'n" and F :: "'b::{field}^'m^'m"
   shows "row i A = 0 \<Longrightarrow> det A = 0" and "row j F = 0 \<Longrightarrow> det F = 0"
   by (force simp: row_def det_def vec_eq_iff sign_nz intro!: sum.neutral)+
 
-lemma%unimportant  det_zero_column:
+lemma  det_zero_column:
   fixes A :: "'a::{idom, ring_char_0}^'n^'n" and F :: "'b::{field}^'m^'m"
   shows "column i A = 0 \<Longrightarrow> det A = 0" and "column j F = 0 \<Longrightarrow> det F = 0"
   unfolding atomize_conj atomize_imp
   by (metis det_transpose det_zero_row row_transpose)
 
-lemma%unimportant  det_row_add:
+lemma  det_row_add:
   fixes a b c :: "'n::finite \<Rightarrow> _ ^ 'n"
   shows "det((\<chi> i. if i = k then a i + b i else c i)::'a::comm_ring_1^'n^'n) =
     det((\<chi> i. if i = k then a i else c i)::'a::comm_ring_1^'n^'n) +
     det((\<chi> i. if i = k then b i else c i)::'a::comm_ring_1^'n^'n)"
   unfolding det_def vec_lambda_beta sum.distrib[symmetric]

   then show "of_int (sign p) * prod (\<lambda>i. ?f i $ p i) ?U =
     of_int (sign p) * prod (\<lambda>i. ?g i $ p i) ?U + of_int (sign p) * prod (\<lambda>i. ?h i $ p i) ?U"
     by (simp add: field_simps)
 qed auto
 
-lemma%unimportant  det_row_mul:
+lemma  det_row_mul:
   fixes a b :: "'n::finite \<Rightarrow> _ ^ 'n"
   shows "det((\<chi> i. if i = k then c *s a i else b i)::'a::comm_ring_1^'n^'n) =
     c * det((\<chi> i. if i = k then a i else b i)::'a::comm_ring_1^'n^'n)"
   unfolding det_def vec_lambda_beta sum_distrib_left
 proof (rule sum.cong)

     unfolding kU[symmetric] .
   then show "of_int (sign p) * prod (\<lambda>i. ?f i $ p i) ?U = c * (of_int (sign p) * prod (\<lambda>i. ?g i $ p i) ?U)"
     by (simp add: field_simps)
 qed auto
 
-lemma%unimportant  det_row_0:
+lemma  det_row_0:
   fixes b :: "'n::finite \<Rightarrow> _ ^ 'n"
   shows "det((\<chi> i. if i = k then 0 else b i)::'a::comm_ring_1^'n^'n) = 0"
   using det_row_mul[of k 0 "\<lambda>i. 1" b]
   apply simp
   apply (simp only: vector_smult_lzero)
   done
 
-lemma%important  det_row_operation:
+lemma  det_row_operation:
   fixes A :: "'a::{comm_ring_1}^'n^'n"
   assumes ij: "i \<noteq> j"
   shows "det (\<chi> k. if k = i then row i A + c *s row j A else row k A) = det A"
-proof%unimportant -
+proof -
   let ?Z = "(\<chi> k. if k = i then row j A else row k A) :: 'a ^'n^'n"
   have th: "row i ?Z = row j ?Z" by (vector row_def)
   have th2: "((\<chi> k. if k = i then row i A else row k A) :: 'a^'n^'n) = A"
     by (vector row_def)
   show ?thesis
     unfolding det_row_add [of i] det_row_mul[of i] det_identical_rows[OF ij th] th2
     by simp
 qed
 
-lemma%unimportant  det_row_span:
+lemma  det_row_span:
   fixes A :: "'a::{field}^'n^'n"
   assumes x: "x \<in> vec.span {row j A |j. j \<noteq> i}"
   shows "det (\<chi> k. if k = i then row i A + x else row k A) = det A"
   using x
 proof (induction rule: vec.span_induct_alt)

     unfolding thz step.IH det_row_mul[of i] det_row_add[of i] by simp
   then show ?case
     unfolding scalar_mult_eq_scaleR .
 qed
 
-lemma%unimportant  matrix_id [simp]: "det (matrix id) = 1"
+lemma  matrix_id [simp]: "det (matrix id) = 1"
   by (simp add: matrix_id_mat_1)
 
-lemma%important  det_matrix_scaleR [simp]: "det (matrix (((*\<^sub>R) r)) :: real^'n^'n) = r ^ CARD('n::finite)"
+proposition  det_matrix_scaleR [simp]: "det (matrix (((*\<^sub>R) r)) :: real^'n^'n) = r ^ CARD('n::finite)"
   apply (subst det_diagonal)
    apply (auto simp: matrix_def mat_def)
   apply (simp add: cart_eq_inner_axis inner_axis_axis)
   done
 
 text \<open>
   May as well do this, though it's a bit unsatisfactory since it ignores
   exact duplicates by considering the rows/columns as a set.
 \<close>
 
-lemma%unimportant  det_dependent_rows:
+lemma  det_dependent_rows:
   fixes A:: "'a::{field}^'n^'n"
   assumes d: "vec.dependent (rows A)"
   shows "det A = 0"
 proof -
   let ?U = "UNIV :: 'n set"

       by auto
     from det_identical_rows[OF jk] show ?thesis .
   qed
 qed
 
-lemma%unimportant  det_dependent_columns:
+lemma  det_dependent_columns:
   assumes d: "vec.dependent (columns (A::real^'n^'n))"
   shows "det A = 0"
   by (metis d det_dependent_rows rows_transpose det_transpose)
 
 text \<open>Multilinearity and the multiplication formula\<close>
 
-lemma%unimportant  Cart_lambda_cong: "(\<And>x. f x = g x) \<Longrightarrow> (vec_lambda f::'a^'n) = (vec_lambda g :: 'a^'n)"
+lemma  Cart_lambda_cong: "(\<And>x. f x = g x) \<Longrightarrow> (vec_lambda f::'a^'n) = (vec_lambda g :: 'a^'n)"
   by auto
 
-lemma%unimportant  det_linear_row_sum:
+lemma  det_linear_row_sum:
   assumes fS: "finite S"
   shows "det ((\<chi> i. if i = k then sum (a i) S else c i)::'a::comm_ring_1^'n^'n) =
     sum (\<lambda>j. det ((\<chi> i. if i = k then a  i j else c i)::'a^'n^'n)) S"
   using fS  by (induct rule: finite_induct; simp add: det_row_0 det_row_add cong: if_cong)
 
-lemma%unimportant  finite_bounded_functions:
+lemma  finite_bounded_functions:
   assumes fS: "finite S"
   shows "finite {f. (\<forall>i \<in> {1.. (k::nat)}. f i \<in> S) \<and> (\<forall>i. i \<notin> {1 .. k} \<longrightarrow> f i = i)}"
 proof (induct k)
   case 0
   have *: "{f. \<forall>i. f i = i} = {id}"

   show ?case
     by metis
 qed
 
 
-lemma%important  det_linear_rows_sum_lemma:
+lemma  det_linear_rows_sum_lemma:
   assumes fS: "finite S"
     and fT: "finite T"
   shows "det ((\<chi> i. if i \<in> T then sum (a i) S else c i):: 'a::comm_ring_1^'n^'n) =
     sum (\<lambda>f. det((\<chi> i. if i \<in> T then a i (f i) else c i)::'a^'n^'n))
       {f. (\<forall>i \<in> T. f i \<in> S) \<and> (\<forall>i. i \<notin> T \<longrightarrow> f i = i)}"
   using fT
-proof%unimportant (induct T arbitrary: a c set: finite)
+proof (induct T arbitrary: a c set: finite)
   case empty
   have th0: "\<And>x y. (\<chi> i. if i \<in> {} then x i else y i) = (\<chi> i. y i)"
     by vector
   from empty.prems show ?case
     unfolding th0 by (simp add: eq_id_iff)

     using \<open>z \<notin> T\<close>
     by (intro sum.reindex_bij_witness[where i="?k" and j="?h"])
        (auto intro!: cong[OF refl[of det]] simp: vec_eq_iff)
 qed
 
-lemma%unimportant  det_linear_rows_sum:
+lemma  det_linear_rows_sum:
   fixes S :: "'n::finite set"
   assumes fS: "finite S"
   shows "det (\<chi> i. sum (a i) S) =
     sum (\<lambda>f. det (\<chi> i. a i (f i) :: 'a::comm_ring_1 ^ 'n^'n)) {f. \<forall>i. f i \<in> S}"
 proof -

     by vector
   from det_linear_rows_sum_lemma[OF fS, of "UNIV :: 'n set" a, unfolded th0, OF finite]
   show ?thesis by simp
 qed
 
-lemma%unimportant  matrix_mul_sum_alt:
+lemma  matrix_mul_sum_alt:
   fixes A B :: "'a::comm_ring_1^'n^'n"
   shows "A ** B = (\<chi> i. sum (\<lambda>k. A$i$k *s B $ k) (UNIV :: 'n set))"
   by (vector matrix_matrix_mult_def sum_component)
 
-lemma%unimportant  det_rows_mul:
+lemma  det_rows_mul:
   "det((\<chi> i. c i *s a i)::'a::comm_ring_1^'n^'n) =
     prod (\<lambda>i. c i) (UNIV:: 'n set) * det((\<chi> i. a i)::'a^'n^'n)"
 proof (simp add: det_def sum_distrib_left cong add: prod.cong, rule sum.cong)
   let ?U = "UNIV :: 'n set"
   let ?PU = "{p. p permutes ?U}"

   then show "?s * (\<Prod>xa\<in>?U. c xa * a xa $ p xa) =
     prod c ?U * (?s* (\<Prod>xa\<in>?U. a xa $ p xa))"
     by (simp add: field_simps)
 qed rule
 
-lemma%important  det_mul:
+proposition  det_mul:
   fixes A B :: "'a::comm_ring_1^'n^'n"
   shows "det (A ** B) = det A * det B"
-proof%unimportant -
+proof -
   let ?U = "UNIV :: 'n set"
   let ?F = "{f. (\<forall>i \<in> ?U. f i \<in> ?U) \<and> (\<forall>i. i \<notin> ?U \<longrightarrow> f i = i)}"
   let ?PU = "{p. p permutes ?U}"
   have "p \<in> ?F" if "p permutes ?U" for p
     by simp

 qed
 
 
 subsection \<open>Relation to invertibility\<close>
 
-lemma%important  invertible_det_nz:
+proposition  invertible_det_nz:
   fixes A::"'a::{field}^'n^'n"
   shows "invertible A \<longleftrightarrow> det A \<noteq> 0"
-proof%unimportant (cases "invertible A")
+proof (cases "invertible A")
   case True
   then obtain B :: "'a^'n^'n" where B: "A ** B = mat 1"
     unfolding invertible_right_inverse by blast
   then have "det (A ** B) = det (mat 1 :: 'a^'n^'n)"
     by simp

   then show ?thesis
     by (simp add: False)
 qed
 
 
-lemma%unimportant  det_nz_iff_inj_gen:
+lemma  det_nz_iff_inj_gen:
   fixes f :: "'a::field^'n \<Rightarrow> 'a::field^'n"
   assumes "Vector_Spaces.linear (*s) (*s) f"
   shows "det (matrix f) \<noteq> 0 \<longleftrightarrow> inj f"
 proof
   assume "det (matrix f) \<noteq> 0"

   show "det (matrix f) \<noteq> 0"
     using vec.linear_injective_left_inverse [OF assms \<open>inj f\<close>]
     by (metis assms invertible_det_nz invertible_left_inverse matrix_compose_gen matrix_id_mat_1)
 qed
 
-lemma%unimportant  det_nz_iff_inj:
+lemma  det_nz_iff_inj:
   fixes f :: "real^'n \<Rightarrow> real^'n"
   assumes "linear f"
   shows "det (matrix f) \<noteq> 0 \<longleftrightarrow> inj f"
   using det_nz_iff_inj_gen[of f] assms
   unfolding linear_matrix_vector_mul_eq .
 
-lemma%unimportant  det_eq_0_rank:
+lemma  det_eq_0_rank:
   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  \<open>Invertibility of matrices and corresponding linear functions\<close>
-
-lemma%important  matrix_left_invertible_gen:
+subsubsection%important  \<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))"
-proof%unimportant safe
+proof safe
   fix B
   assume 1: "B ** matrix f = mat 1"
   show "\<exists>g. Vector_Spaces.linear (*s) (*s) g \<and> g \<circ> f = id"
   proof (intro exI conjI)
     show "Vector_Spaces.linear (*s) (*s) (\<lambda>y. B *v y)"

   then have "matrix g ** matrix f = mat 1"
     by (metis assms matrix_compose_gen matrix_id_mat_1)
   then show "\<exists>B. B ** matrix f = mat 1" ..
 qed
 
-lemma%unimportant  matrix_left_invertible:
+lemma  matrix_left_invertible:
   "linear f \<Longrightarrow> ((\<exists>B. B ** matrix f = mat 1) \<longleftrightarrow> (\<exists>g. linear g \<and> g \<circ> f = id))" for f::"real^'m \<Rightarrow> real^'n"
   using matrix_left_invertible_gen[of f]
   by (auto simp: linear_matrix_vector_mul_eq)
 
-lemma%unimportant  matrix_right_invertible_gen:
+lemma  matrix_right_invertible_gen:
   fixes f :: "'a::field^'m \<Rightarrow> 'a^'n"
   assumes "Vector_Spaces.linear (*s) (*s) f"
   shows "((\<exists>B. matrix f ** B = mat 1) \<longleftrightarrow> (\<exists>g. Vector_Spaces.linear (*s) (*s) g \<and> f \<circ> g = id))"
 proof safe
   fix B

   then have "matrix f ** matrix g = mat 1"
     by (metis assms matrix_compose_gen matrix_id_mat_1)
   then show "\<exists>B. matrix f ** B = mat 1" ..
 qed
 
-lemma%unimportant  matrix_right_invertible:
+lemma  matrix_right_invertible:
   "linear f \<Longrightarrow> ((\<exists>B. matrix f ** B = mat 1) \<longleftrightarrow> (\<exists>g. linear g \<and> f \<circ> g = id))" for f::"real^'m \<Rightarrow> real^'n"
   using matrix_right_invertible_gen[of f]
   by (auto simp: linear_matrix_vector_mul_eq)
 
-lemma%unimportant  matrix_invertible_gen:
+lemma  matrix_invertible_gen:
   fixes f :: "'a::field^'m \<Rightarrow> 'a::field^'n"
   assumes "Vector_Spaces.linear (*s) (*s) f"
   shows  "invertible (matrix f) \<longleftrightarrow> (\<exists>g. Vector_Spaces.linear (*s) (*s) g \<and> f \<circ> g = id \<and> g \<circ> f = id)"
     (is "?lhs = ?rhs")
 proof

 next
   assume ?rhs then show ?lhs
     by (metis assms invertible_def matrix_compose_gen matrix_id_mat_1)
 qed
 
-lemma%unimportant  matrix_invertible:
+lemma  matrix_invertible:
   "linear f \<Longrightarrow> invertible (matrix f) \<longleftrightarrow> (\<exists>g. linear g \<and> f \<circ> g = id \<and> g \<circ> f = id)"
   for f::"real^'m \<Rightarrow> real^'n"
   using matrix_invertible_gen[of f]
   by (auto simp: linear_matrix_vector_mul_eq)
 
-lemma%unimportant  invertible_eq_bij:
+lemma  invertible_eq_bij:
   fixes m :: "'a::field^'m^'n"
   shows "invertible m \<longleftrightarrow> bij ((*v) m)"
   using matrix_invertible_gen[OF matrix_vector_mul_linear_gen, of m, simplified matrix_of_matrix_vector_mul]
   by (metis bij_betw_def left_right_inverse_eq matrix_vector_mul_linear_gen o_bij
       vec.linear_injective_left_inverse vec.linear_surjective_right_inverse)
 
 
 subsection \<open>Cramer's rule\<close>
 
-lemma%important  cramer_lemma_transpose:
+lemma  cramer_lemma_transpose:
   fixes A:: "'a::{field}^'n^'n"
     and x :: "'a::{field}^'n"
   shows "det ((\<chi> i. if i = k then sum (\<lambda>i. x$i *s row i A) (UNIV::'n set)
                              else row i A)::'a::{field}^'n^'n) = x$k * det A"
   (is "?lhs = ?rhs")
-proof%unimportant -
+proof -
   let ?U = "UNIV :: 'n set"
   let ?Uk = "?U - {k}"
   have U: "?U = insert k ?Uk"
     by blast
   have kUk: "k \<notin> ?Uk"

     unfolding thd1
     apply (simp add: field_simps)
     done
 qed
 
-lemma%important  cramer_lemma:
+proposition  cramer_lemma:
   fixes A :: "'a::{field}^'n^'n"
   shows "det((\<chi> i j. if j = k then (A *v x)$i else A$i$j):: 'a::{field}^'n^'n) = x$k * det A"
-proof%unimportant -
+proof -
   let ?U = "UNIV :: 'n set"
   have *: "\<And>c. sum (\<lambda>i. c i *s row i (transpose A)) ?U = sum (\<lambda>i. c i *s column i A) ?U"
     by (auto intro: sum.cong)
   show ?thesis
     unfolding matrix_mult_sum

     apply (rule cong[OF refl[of det]])
     apply (vector transpose_def column_def row_def)
     done
 qed
 
-lemma%important  cramer:
+proposition  cramer:
   fixes A ::"'a::{field}^'n^'n"
   assumes d0: "det A \<noteq> 0"
   shows "A *v x = b \<longleftrightarrow> x = (\<chi> k. det(\<chi> i j. if j=k then b$i else A$i$j) / det A)"
-proof%unimportant -
+proof -
   from d0 obtain B where B: "A ** B = mat 1" "B ** A = mat 1"
     unfolding invertible_det_nz[symmetric] invertible_def
     by blast
   have "(A ** B) *v b = b"
     by (simp add: B)

   }
   with xe show ?thesis
     by auto
 qed
 
-lemma%unimportant  det_1: "det (A::'a::comm_ring_1^1^1) = A$1$1"
+lemma  det_1: "det (A::'a::comm_ring_1^1^1) = A$1$1"
   by (simp add: det_def sign_id)
 
-lemma%unimportant  det_2: "det (A::'a::comm_ring_1^2^2) = A$1$1 * A$2$2 - A$1$2 * A$2$1"
+lemma  det_2: "det (A::'a::comm_ring_1^2^2) = A$1$1 * A$2$2 - A$1$2 * A$2$1"
 proof -
   have f12: "finite {2::2}" "1 \<notin> {2::2}" by auto
   show ?thesis
     unfolding det_def UNIV_2
     unfolding sum_over_permutations_insert[OF f12]
     unfolding permutes_sing
     by (simp add: sign_swap_id sign_id swap_id_eq)
 qed
 
-lemma%unimportant  det_3:
+lemma  det_3:
   "det (A::'a::comm_ring_1^3^3) =
     A$1$1 * A$2$2 * A$3$3 +
     A$1$2 * A$2$3 * A$3$1 +
     A$1$3 * A$2$1 * A$3$2 -
     A$1$1 * A$2$3 * A$3$2 -

     unfolding sum_over_permutations_insert[OF f23]
     unfolding permutes_sing
     by (simp add: sign_swap_id permutation_swap_id sign_compose sign_id swap_id_eq)
 qed
 
-lemma%important  det_orthogonal_matrix:
+proposition  det_orthogonal_matrix:
   fixes Q:: "'a::linordered_idom^'n^'n"
   assumes oQ: "orthogonal_matrix Q"
   shows "det Q = 1 \<or> det Q = - 1"
-proof%unimportant -
+proof -
   have "Q ** transpose Q = mat 1"
     by (metis oQ orthogonal_matrix_def)
   then have "det (Q ** transpose Q) = det (mat 1:: 'a^'n^'n)"
     by simp
   then have "det Q * det Q = 1"
     by (simp add: det_mul)
   then show ?thesis
     by (simp add: square_eq_1_iff)
 qed
 
-lemma%important  orthogonal_transformation_det [simp]:
+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
 
 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"
 
-lemma%important  orthogonal_rotation_or_rotoinversion:
+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%unimportant (metis rotoinversion_matrix_def rotation_matrix_def det_orthogonal_matrix)
+  by (metis rotoinversion_matrix_def rotation_matrix_def det_orthogonal_matrix)
 
 text\<open> Slightly stronger results giving rotation, but only in two or more dimensions\<close>
 
-lemma%unimportant  rotation_matrix_exists_basis:
+lemma  rotation_matrix_exists_basis:
   fixes a :: "real^'n"
   assumes 2: "2 \<le> CARD('n)" and "norm a = 1"
   obtains A where "rotation_matrix A" "A *v (axis k 1) = a"
 proof -
   obtain A where "orthogonal_matrix A" and A: "A *v (axis k 1) = a"

         using \<open>j \<noteq> k\<close> A by (simp add: matrix_vector_column axis_def scalar_mult_eq_scaleR if_distrib [of "\<lambda>z. z *\<^sub>R c" for c] cong: if_cong)
     qed
   qed
 qed
 
-lemma%unimportant  rotation_exists_1:
+lemma  rotation_exists_1:
   fixes a :: "real^'n"
   assumes "2 \<le> CARD('n)" "norm a = 1" "norm b = 1"
   obtains f where "orthogonal_transformation f" "det(matrix f) = 1" "f a = b"
 proof -
   obtain k::'n where True

       using AB unfolding orthogonal_matrix_def rotation_matrix_def
       by (metis eq matrix_mul_rid matrix_vector_mul_assoc)
   qed
 qed
 
-lemma%unimportant  rotation_exists:
+lemma  rotation_exists:
   fixes a :: "real^'n"
   assumes 2: "2 \<le> CARD('n)" and eq: "norm a = norm b"
   obtains f where "orthogonal_transformation f" "det(matrix f) = 1" "f a = b"
 proof (cases "a = 0 \<or> b = 0")
   case True

     using f' False
     by (simp add: eq scale)
   with f show thesis ..
 qed
 
-lemma%unimportant  rotation_rightward_line:
+lemma  rotation_rightward_line:
   fixes a :: "real^'n"
   obtains f where "orthogonal_transformation f" "2 \<le> CARD('n) \<Longrightarrow> det(matrix f) = 1"
                   "f(norm a *\<^sub>R axis k 1) = a"
 proof (cases "CARD('n) = 1")
   case True