src/HOL/Analysis/Determinants.thy
changeset 68833 fde093888c16
parent 68263 e4e536a71e3d
child 69064 5840724b1d71
     1.1 --- a/src/HOL/Analysis/Determinants.thy	Mon Aug 27 22:58:36 2018 +0200
     1.2 +++ b/src/HOL/Analysis/Determinants.thy	Tue Aug 28 13:28:39 2018 +0100
     1.3 @@ -10,40 +10,40 @@
     1.4    "HOL-Library.Permutations"
     1.5  begin
     1.6  
     1.7 -subsection \<open>Trace\<close>
     1.8 +subsection%important  \<open>Trace\<close>
     1.9  
    1.10 -definition trace :: "'a::semiring_1^'n^'n \<Rightarrow> 'a"
    1.11 +definition%important  trace :: "'a::semiring_1^'n^'n \<Rightarrow> 'a"
    1.12    where "trace A = sum (\<lambda>i. ((A$i)$i)) (UNIV::'n set)"
    1.13  
    1.14 -lemma trace_0: "trace (mat 0) = 0"
    1.15 +lemma%unimportant  trace_0: "trace (mat 0) = 0"
    1.16    by (simp add: trace_def mat_def)
    1.17  
    1.18 -lemma trace_I: "trace (mat 1 :: 'a::semiring_1^'n^'n) = of_nat(CARD('n))"
    1.19 +lemma%unimportant  trace_I: "trace (mat 1 :: 'a::semiring_1^'n^'n) = of_nat(CARD('n))"
    1.20    by (simp add: trace_def mat_def)
    1.21  
    1.22 -lemma trace_add: "trace ((A::'a::comm_semiring_1^'n^'n) + B) = trace A + trace B"
    1.23 +lemma%unimportant  trace_add: "trace ((A::'a::comm_semiring_1^'n^'n) + B) = trace A + trace B"
    1.24    by (simp add: trace_def sum.distrib)
    1.25  
    1.26 -lemma trace_sub: "trace ((A::'a::comm_ring_1^'n^'n) - B) = trace A - trace B"
    1.27 +lemma%unimportant  trace_sub: "trace ((A::'a::comm_ring_1^'n^'n) - B) = trace A - trace B"
    1.28    by (simp add: trace_def sum_subtractf)
    1.29  
    1.30 -lemma trace_mul_sym: "trace ((A::'a::comm_semiring_1^'n^'m) ** B) = trace (B**A)"
    1.31 +lemma%important  trace_mul_sym: "trace ((A::'a::comm_semiring_1^'n^'m) ** B) = trace (B**A)"
    1.32    apply (simp add: trace_def matrix_matrix_mult_def)
    1.33    apply (subst sum.swap)
    1.34    apply (simp add: mult.commute)
    1.35    done
    1.36  
    1.37 -subsubsection \<open>Definition of determinant\<close>
    1.38 +subsubsection%important  \<open>Definition of determinant\<close>
    1.39  
    1.40 -definition det:: "'a::comm_ring_1^'n^'n \<Rightarrow> 'a" where
    1.41 +definition%important  det:: "'a::comm_ring_1^'n^'n \<Rightarrow> 'a" where
    1.42    "det A =
    1.43      sum (\<lambda>p. of_int (sign p) * prod (\<lambda>i. A$i$p i) (UNIV :: 'n set))
    1.44        {p. p permutes (UNIV :: 'n set)}"
    1.45  
    1.46  text \<open>Basic determinant properties\<close>
    1.47  
    1.48 -lemma det_transpose [simp]: "det (transpose A) = det (A::'a::comm_ring_1 ^'n^'n)"
    1.49 -proof -
    1.50 +lemma%important  det_transpose [simp]: "det (transpose A) = det (A::'a::comm_ring_1 ^'n^'n)"
    1.51 +proof%unimportant -
    1.52    let ?di = "\<lambda>A i j. A$i$j"
    1.53    let ?U = "(UNIV :: 'n set)"
    1.54    have fU: "finite ?U" by simp
    1.55 @@ -80,7 +80,7 @@
    1.56      by (subst sum_permutations_inverse) (blast intro: sum.cong)
    1.57  qed
    1.58  
    1.59 -lemma det_lowerdiagonal:
    1.60 +lemma%unimportant  det_lowerdiagonal:
    1.61    fixes A :: "'a::comm_ring_1^('n::{finite,wellorder})^('n::{finite,wellorder})"
    1.62    assumes ld: "\<And>i j. i < j \<Longrightarrow> A$i$j = 0"
    1.63    shows "det A = prod (\<lambda>i. A$i$i) (UNIV:: 'n set)"
    1.64 @@ -107,11 +107,11 @@
    1.65      unfolding det_def by (simp add: sign_id)
    1.66  qed
    1.67  
    1.68 -lemma det_upperdiagonal:
    1.69 +lemma%important  det_upperdiagonal:
    1.70    fixes A :: "'a::comm_ring_1^'n::{finite,wellorder}^'n::{finite,wellorder}"
    1.71    assumes ld: "\<And>i j. i > j \<Longrightarrow> A$i$j = 0"
    1.72    shows "det A = prod (\<lambda>i. A$i$i) (UNIV:: 'n set)"
    1.73 -proof -
    1.74 +proof%unimportant -
    1.75    let ?U = "UNIV:: 'n set"
    1.76    let ?PU = "{p. p permutes ?U}"
    1.77    let ?pp = "(\<lambda>p. of_int (sign p) * prod (\<lambda>i. A$i$p i) (UNIV :: 'n set))"
    1.78 @@ -134,11 +134,11 @@
    1.79      unfolding det_def by (simp add: sign_id)
    1.80  qed
    1.81  
    1.82 -lemma det_diagonal:
    1.83 +lemma%important  det_diagonal:
    1.84    fixes A :: "'a::comm_ring_1^'n^'n"
    1.85    assumes ld: "\<And>i j. i \<noteq> j \<Longrightarrow> A$i$j = 0"
    1.86    shows "det A = prod (\<lambda>i. A$i$i) (UNIV::'n set)"
    1.87 -proof -
    1.88 +proof%unimportant -
    1.89    let ?U = "UNIV:: 'n set"
    1.90    let ?PU = "{p. p permutes ?U}"
    1.91    let ?pp = "\<lambda>p. of_int (sign p) * prod (\<lambda>i. A$i$p i) (UNIV :: 'n set)"
    1.92 @@ -161,13 +161,13 @@
    1.93      unfolding det_def by (simp add: sign_id)
    1.94  qed
    1.95  
    1.96 -lemma det_I [simp]: "det (mat 1 :: 'a::comm_ring_1^'n^'n) = 1"
    1.97 +lemma%unimportant  det_I [simp]: "det (mat 1 :: 'a::comm_ring_1^'n^'n) = 1"
    1.98    by (simp add: det_diagonal mat_def)
    1.99  
   1.100 -lemma det_0 [simp]: "det (mat 0 :: 'a::comm_ring_1^'n^'n) = 0"
   1.101 +lemma%unimportant  det_0 [simp]: "det (mat 0 :: 'a::comm_ring_1^'n^'n) = 0"
   1.102    by (simp add: det_def prod_zero power_0_left)
   1.103  
   1.104 -lemma det_permute_rows:
   1.105 +lemma%unimportant  det_permute_rows:
   1.106    fixes A :: "'a::comm_ring_1^'n^'n"
   1.107    assumes p: "p permutes (UNIV :: 'n::finite set)"
   1.108    shows "det (\<chi> i. A$p i :: 'a^'n^'n) = of_int (sign p) * det A"
   1.109 @@ -204,11 +204,11 @@
   1.110      done
   1.111  qed
   1.112  
   1.113 -lemma det_permute_columns:
   1.114 +lemma%important  det_permute_columns:
   1.115    fixes A :: "'a::comm_ring_1^'n^'n"
   1.116    assumes p: "p permutes (UNIV :: 'n set)"
   1.117    shows "det(\<chi> i j. A$i$ p j :: 'a^'n^'n) = of_int (sign p) * det A"
   1.118 -proof -
   1.119 +proof%unimportant -
   1.120    let ?Ap = "\<chi> i j. A$i$ p j :: 'a^'n^'n"
   1.121    let ?At = "transpose A"
   1.122    have "of_int (sign p) * det A = det (transpose (\<chi> i. transpose A $ p i))"
   1.123 @@ -220,7 +220,7 @@
   1.124      by simp
   1.125  qed
   1.126  
   1.127 -lemma det_identical_columns:
   1.128 +lemma%unimportant  det_identical_columns:
   1.129    fixes A :: "'a::comm_ring_1^'n^'n"
   1.130    assumes jk: "j \<noteq> k"
   1.131      and r: "column j A = column k A"
   1.132 @@ -300,24 +300,24 @@
   1.133    finally show "det A = 0" by simp
   1.134  qed
   1.135  
   1.136 -lemma det_identical_rows:
   1.137 +lemma%unimportant  det_identical_rows:
   1.138    fixes A :: "'a::comm_ring_1^'n^'n"
   1.139    assumes ij: "i \<noteq> j" and r: "row i A = row j A"
   1.140    shows "det A = 0"
   1.141    by (metis column_transpose det_identical_columns det_transpose ij r)
   1.142  
   1.143 -lemma det_zero_row:
   1.144 +lemma%unimportant  det_zero_row:
   1.145    fixes A :: "'a::{idom, ring_char_0}^'n^'n" and F :: "'b::{field}^'m^'m"
   1.146    shows "row i A = 0 \<Longrightarrow> det A = 0" and "row j F = 0 \<Longrightarrow> det F = 0"
   1.147    by (force simp: row_def det_def vec_eq_iff sign_nz intro!: sum.neutral)+
   1.148  
   1.149 -lemma det_zero_column:
   1.150 +lemma%unimportant  det_zero_column:
   1.151    fixes A :: "'a::{idom, ring_char_0}^'n^'n" and F :: "'b::{field}^'m^'m"
   1.152    shows "column i A = 0 \<Longrightarrow> det A = 0" and "column j F = 0 \<Longrightarrow> det F = 0"
   1.153    unfolding atomize_conj atomize_imp
   1.154    by (metis det_transpose det_zero_row row_transpose)
   1.155  
   1.156 -lemma det_row_add:
   1.157 +lemma%unimportant  det_row_add:
   1.158    fixes a b c :: "'n::finite \<Rightarrow> _ ^ 'n"
   1.159    shows "det((\<chi> i. if i = k then a i + b i else c i)::'a::comm_ring_1^'n^'n) =
   1.160      det((\<chi> i. if i = k then a i else c i)::'a::comm_ring_1^'n^'n) +
   1.161 @@ -358,7 +358,7 @@
   1.162      by (simp add: field_simps)
   1.163  qed auto
   1.164  
   1.165 -lemma det_row_mul:
   1.166 +lemma%unimportant  det_row_mul:
   1.167    fixes a b :: "'n::finite \<Rightarrow> _ ^ 'n"
   1.168    shows "det((\<chi> i. if i = k then c *s a i else b i)::'a::comm_ring_1^'n^'n) =
   1.169      c * det((\<chi> i. if i = k then a i else b i)::'a::comm_ring_1^'n^'n)"
   1.170 @@ -395,7 +395,7 @@
   1.171      by (simp add: field_simps)
   1.172  qed auto
   1.173  
   1.174 -lemma det_row_0:
   1.175 +lemma%unimportant  det_row_0:
   1.176    fixes b :: "'n::finite \<Rightarrow> _ ^ 'n"
   1.177    shows "det((\<chi> i. if i = k then 0 else b i)::'a::comm_ring_1^'n^'n) = 0"
   1.178    using det_row_mul[of k 0 "\<lambda>i. 1" b]
   1.179 @@ -403,11 +403,11 @@
   1.180    apply (simp only: vector_smult_lzero)
   1.181    done
   1.182  
   1.183 -lemma det_row_operation:
   1.184 +lemma%important  det_row_operation:
   1.185    fixes A :: "'a::{comm_ring_1}^'n^'n"
   1.186    assumes ij: "i \<noteq> j"
   1.187    shows "det (\<chi> k. if k = i then row i A + c *s row j A else row k A) = det A"
   1.188 -proof -
   1.189 +proof%unimportant -
   1.190    let ?Z = "(\<chi> k. if k = i then row j A else row k A) :: 'a ^'n^'n"
   1.191    have th: "row i ?Z = row j ?Z" by (vector row_def)
   1.192    have th2: "((\<chi> k. if k = i then row i A else row k A) :: 'a^'n^'n) = A"
   1.193 @@ -417,7 +417,7 @@
   1.194      by simp
   1.195  qed
   1.196  
   1.197 -lemma det_row_span:
   1.198 +lemma%unimportant  det_row_span:
   1.199    fixes A :: "'a::{field}^'n^'n"
   1.200    assumes x: "x \<in> vec.span {row j A |j. j \<noteq> i}"
   1.201    shows "det (\<chi> k. if k = i then row i A + x else row k A) = det A"
   1.202 @@ -449,10 +449,10 @@
   1.203      unfolding scalar_mult_eq_scaleR .
   1.204  qed
   1.205  
   1.206 -lemma matrix_id [simp]: "det (matrix id) = 1"
   1.207 +lemma%unimportant  matrix_id [simp]: "det (matrix id) = 1"
   1.208    by (simp add: matrix_id_mat_1)
   1.209  
   1.210 -lemma det_matrix_scaleR [simp]: "det (matrix ((( *\<^sub>R) r)) :: real^'n^'n) = r ^ CARD('n::finite)"
   1.211 +lemma%important  det_matrix_scaleR [simp]: "det (matrix ((( *\<^sub>R) r)) :: real^'n^'n) = r ^ CARD('n::finite)"
   1.212    apply (subst det_diagonal)
   1.213     apply (auto simp: matrix_def mat_def)
   1.214    apply (simp add: cart_eq_inner_axis inner_axis_axis)
   1.215 @@ -463,7 +463,7 @@
   1.216    exact duplicates by considering the rows/columns as a set.
   1.217  \<close>
   1.218  
   1.219 -lemma det_dependent_rows:
   1.220 +lemma%unimportant  det_dependent_rows:
   1.221    fixes A:: "'a::{field}^'n^'n"
   1.222    assumes d: "vec.dependent (rows A)"
   1.223    shows "det A = 0"
   1.224 @@ -491,23 +491,23 @@
   1.225    qed
   1.226  qed
   1.227  
   1.228 -lemma det_dependent_columns:
   1.229 +lemma%unimportant  det_dependent_columns:
   1.230    assumes d: "vec.dependent (columns (A::real^'n^'n))"
   1.231    shows "det A = 0"
   1.232    by (metis d det_dependent_rows rows_transpose det_transpose)
   1.233  
   1.234  text \<open>Multilinearity and the multiplication formula\<close>
   1.235  
   1.236 -lemma Cart_lambda_cong: "(\<And>x. f x = g x) \<Longrightarrow> (vec_lambda f::'a^'n) = (vec_lambda g :: 'a^'n)"
   1.237 +lemma%unimportant  Cart_lambda_cong: "(\<And>x. f x = g x) \<Longrightarrow> (vec_lambda f::'a^'n) = (vec_lambda g :: 'a^'n)"
   1.238    by auto
   1.239  
   1.240 -lemma det_linear_row_sum:
   1.241 +lemma%unimportant  det_linear_row_sum:
   1.242    assumes fS: "finite S"
   1.243    shows "det ((\<chi> i. if i = k then sum (a i) S else c i)::'a::comm_ring_1^'n^'n) =
   1.244      sum (\<lambda>j. det ((\<chi> i. if i = k then a  i j else c i)::'a^'n^'n)) S"
   1.245    using fS  by (induct rule: finite_induct; simp add: det_row_0 det_row_add cong: if_cong)
   1.246  
   1.247 -lemma finite_bounded_functions:
   1.248 +lemma%unimportant  finite_bounded_functions:
   1.249    assumes fS: "finite S"
   1.250    shows "finite {f. (\<forall>i \<in> {1.. (k::nat)}. f i \<in> S) \<and> (\<forall>i. i \<notin> {1 .. k} \<longrightarrow> f i = i)}"
   1.251  proof (induct k)
   1.252 @@ -532,14 +532,14 @@
   1.253  qed
   1.254  
   1.255  
   1.256 -lemma det_linear_rows_sum_lemma:
   1.257 +lemma%important  det_linear_rows_sum_lemma:
   1.258    assumes fS: "finite S"
   1.259      and fT: "finite T"
   1.260    shows "det ((\<chi> i. if i \<in> T then sum (a i) S else c i):: 'a::comm_ring_1^'n^'n) =
   1.261      sum (\<lambda>f. det((\<chi> i. if i \<in> T then a i (f i) else c i)::'a^'n^'n))
   1.262        {f. (\<forall>i \<in> T. f i \<in> S) \<and> (\<forall>i. i \<notin> T \<longrightarrow> f i = i)}"
   1.263    using fT
   1.264 -proof (induct T arbitrary: a c set: finite)
   1.265 +proof%unimportant (induct T arbitrary: a c set: finite)
   1.266    case empty
   1.267    have th0: "\<And>x y. (\<chi> i. if i \<in> {} then x i else y i) = (\<chi> i. y i)"
   1.268      by vector
   1.269 @@ -577,7 +577,7 @@
   1.270         (auto intro!: cong[OF refl[of det]] simp: vec_eq_iff)
   1.271  qed
   1.272  
   1.273 -lemma det_linear_rows_sum:
   1.274 +lemma%unimportant  det_linear_rows_sum:
   1.275    fixes S :: "'n::finite set"
   1.276    assumes fS: "finite S"
   1.277    shows "det (\<chi> i. sum (a i) S) =
   1.278 @@ -589,12 +589,12 @@
   1.279    show ?thesis by simp
   1.280  qed
   1.281  
   1.282 -lemma matrix_mul_sum_alt:
   1.283 +lemma%unimportant  matrix_mul_sum_alt:
   1.284    fixes A B :: "'a::comm_ring_1^'n^'n"
   1.285    shows "A ** B = (\<chi> i. sum (\<lambda>k. A$i$k *s B $ k) (UNIV :: 'n set))"
   1.286    by (vector matrix_matrix_mult_def sum_component)
   1.287  
   1.288 -lemma det_rows_mul:
   1.289 +lemma%unimportant  det_rows_mul:
   1.290    "det((\<chi> i. c i *s a i)::'a::comm_ring_1^'n^'n) =
   1.291      prod (\<lambda>i. c i) (UNIV:: 'n set) * det((\<chi> i. a i)::'a^'n^'n)"
   1.292  proof (simp add: det_def sum_distrib_left cong add: prod.cong, rule sum.cong)
   1.293 @@ -612,10 +612,10 @@
   1.294      by (simp add: field_simps)
   1.295  qed rule
   1.296  
   1.297 -lemma det_mul:
   1.298 +lemma%important  det_mul:
   1.299    fixes A B :: "'a::comm_ring_1^'n^'n"
   1.300    shows "det (A ** B) = det A * det B"
   1.301 -proof -
   1.302 +proof%unimportant -
   1.303    let ?U = "UNIV :: 'n set"
   1.304    let ?F = "{f. (\<forall>i \<in> ?U. f i \<in> ?U) \<and> (\<forall>i. i \<notin> ?U \<longrightarrow> f i = i)}"
   1.305    let ?PU = "{p. p permutes ?U}"
   1.306 @@ -712,12 +712,12 @@
   1.307  qed
   1.308  
   1.309  
   1.310 -subsection \<open>Relation to invertibility\<close>
   1.311 +subsection%important \<open>Relation to invertibility\<close>
   1.312  
   1.313 -lemma invertible_det_nz:
   1.314 +lemma%important  invertible_det_nz:
   1.315    fixes A::"'a::{field}^'n^'n"
   1.316    shows "invertible A \<longleftrightarrow> det A \<noteq> 0"
   1.317 -proof (cases "invertible A")
   1.318 +proof%unimportant (cases "invertible A")
   1.319    case True
   1.320    then obtain B :: "'a^'n^'n" where B: "A ** B = mat 1"
   1.321      unfolding invertible_right_inverse by blast
   1.322 @@ -748,7 +748,7 @@
   1.323  qed
   1.324  
   1.325  
   1.326 -lemma det_nz_iff_inj_gen:
   1.327 +lemma%unimportant  det_nz_iff_inj_gen:
   1.328    fixes f :: "'a::field^'n \<Rightarrow> 'a::field^'n"
   1.329    assumes "Vector_Spaces.linear ( *s) ( *s) f"
   1.330    shows "det (matrix f) \<noteq> 0 \<longleftrightarrow> inj f"
   1.331 @@ -763,26 +763,26 @@
   1.332      by (metis assms invertible_det_nz invertible_left_inverse matrix_compose_gen matrix_id_mat_1)
   1.333  qed
   1.334  
   1.335 -lemma det_nz_iff_inj:
   1.336 +lemma%unimportant  det_nz_iff_inj:
   1.337    fixes f :: "real^'n \<Rightarrow> real^'n"
   1.338    assumes "linear f"
   1.339    shows "det (matrix f) \<noteq> 0 \<longleftrightarrow> inj f"
   1.340    using det_nz_iff_inj_gen[of f] assms
   1.341    unfolding linear_matrix_vector_mul_eq .
   1.342  
   1.343 -lemma det_eq_0_rank:
   1.344 +lemma%unimportant  det_eq_0_rank:
   1.345    fixes A :: "real^'n^'n"
   1.346    shows "det A = 0 \<longleftrightarrow> rank A < CARD('n)"
   1.347    using invertible_det_nz [of A]
   1.348    by (auto simp: matrix_left_invertible_injective invertible_left_inverse less_rank_noninjective)
   1.349  
   1.350 -subsubsection\<open>Invertibility of matrices and corresponding linear functions\<close>
   1.351 +subsubsection%important  \<open>Invertibility of matrices and corresponding linear functions\<close>
   1.352  
   1.353 -lemma matrix_left_invertible_gen:
   1.354 +lemma%important  matrix_left_invertible_gen:
   1.355    fixes f :: "'a::field^'m \<Rightarrow> 'a::field^'n"
   1.356    assumes "Vector_Spaces.linear ( *s) ( *s) f"
   1.357    shows "((\<exists>B. B ** matrix f = mat 1) \<longleftrightarrow> (\<exists>g. Vector_Spaces.linear ( *s) ( *s) g \<and> g \<circ> f = id))"
   1.358 -proof safe
   1.359 +proof%unimportant safe
   1.360    fix B
   1.361    assume 1: "B ** matrix f = mat 1"
   1.362    show "\<exists>g. Vector_Spaces.linear ( *s) ( *s) g \<and> g \<circ> f = id"
   1.363 @@ -801,12 +801,12 @@
   1.364    then show "\<exists>B. B ** matrix f = mat 1" ..
   1.365  qed
   1.366  
   1.367 -lemma matrix_left_invertible:
   1.368 +lemma%unimportant  matrix_left_invertible:
   1.369    "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"
   1.370    using matrix_left_invertible_gen[of f]
   1.371    by (auto simp: linear_matrix_vector_mul_eq)
   1.372  
   1.373 -lemma matrix_right_invertible_gen:
   1.374 +lemma%unimportant  matrix_right_invertible_gen:
   1.375    fixes f :: "'a::field^'m \<Rightarrow> 'a^'n"
   1.376    assumes "Vector_Spaces.linear ( *s) ( *s) f"
   1.377    shows "((\<exists>B. matrix f ** B = mat 1) \<longleftrightarrow> (\<exists>g. Vector_Spaces.linear ( *s) ( *s) g \<and> f \<circ> g = id))"
   1.378 @@ -829,12 +829,12 @@
   1.379    then show "\<exists>B. matrix f ** B = mat 1" ..
   1.380  qed
   1.381  
   1.382 -lemma matrix_right_invertible:
   1.383 +lemma%unimportant  matrix_right_invertible:
   1.384    "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"
   1.385    using matrix_right_invertible_gen[of f]
   1.386    by (auto simp: linear_matrix_vector_mul_eq)
   1.387  
   1.388 -lemma matrix_invertible_gen:
   1.389 +lemma%unimportant  matrix_invertible_gen:
   1.390    fixes f :: "'a::field^'m \<Rightarrow> 'a::field^'n"
   1.391    assumes "Vector_Spaces.linear ( *s) ( *s) f"
   1.392    shows  "invertible (matrix f) \<longleftrightarrow> (\<exists>g. Vector_Spaces.linear ( *s) ( *s) g \<and> f \<circ> g = id \<and> g \<circ> f = id)"
   1.393 @@ -847,13 +847,13 @@
   1.394      by (metis assms invertible_def matrix_compose_gen matrix_id_mat_1)
   1.395  qed
   1.396  
   1.397 -lemma matrix_invertible:
   1.398 +lemma%unimportant  matrix_invertible:
   1.399    "linear f \<Longrightarrow> invertible (matrix f) \<longleftrightarrow> (\<exists>g. linear g \<and> f \<circ> g = id \<and> g \<circ> f = id)"
   1.400    for f::"real^'m \<Rightarrow> real^'n"
   1.401    using matrix_invertible_gen[of f]
   1.402    by (auto simp: linear_matrix_vector_mul_eq)
   1.403  
   1.404 -lemma invertible_eq_bij:
   1.405 +lemma%unimportant  invertible_eq_bij:
   1.406    fixes m :: "'a::field^'m^'n"
   1.407    shows "invertible m \<longleftrightarrow> bij (( *v) m)"
   1.408    using matrix_invertible_gen[OF matrix_vector_mul_linear_gen, of m, simplified matrix_of_matrix_vector_mul]
   1.409 @@ -861,15 +861,15 @@
   1.410        vec.linear_injective_left_inverse vec.linear_surjective_right_inverse)
   1.411  
   1.412  
   1.413 -subsection \<open>Cramer's rule\<close>
   1.414 +subsection%important \<open>Cramer's rule\<close>
   1.415  
   1.416 -lemma cramer_lemma_transpose:
   1.417 +lemma%important  cramer_lemma_transpose:
   1.418    fixes A:: "'a::{field}^'n^'n"
   1.419      and x :: "'a::{field}^'n"
   1.420    shows "det ((\<chi> i. if i = k then sum (\<lambda>i. x$i *s row i A) (UNIV::'n set)
   1.421                               else row i A)::'a::{field}^'n^'n) = x$k * det A"
   1.422    (is "?lhs = ?rhs")
   1.423 -proof -
   1.424 +proof%unimportant -
   1.425    let ?U = "UNIV :: 'n set"
   1.426    let ?Uk = "?U - {k}"
   1.427    have U: "?U = insert k ?Uk"
   1.428 @@ -899,10 +899,10 @@
   1.429      done
   1.430  qed
   1.431  
   1.432 -lemma cramer_lemma:
   1.433 +lemma%important  cramer_lemma:
   1.434    fixes A :: "'a::{field}^'n^'n"
   1.435    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"
   1.436 -proof -
   1.437 +proof%unimportant -
   1.438    let ?U = "UNIV :: 'n set"
   1.439    have *: "\<And>c. sum (\<lambda>i. c i *s row i (transpose A)) ?U = sum (\<lambda>i. c i *s column i A) ?U"
   1.440      by (auto intro: sum.cong)
   1.441 @@ -916,11 +916,11 @@
   1.442      done
   1.443  qed
   1.444  
   1.445 -lemma cramer:
   1.446 +lemma%important  cramer:
   1.447    fixes A ::"'a::{field}^'n^'n"
   1.448    assumes d0: "det A \<noteq> 0"
   1.449    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)"
   1.450 -proof -
   1.451 +proof%unimportant -
   1.452    from d0 obtain B where B: "A ** B = mat 1" "B ** A = mat 1"
   1.453      unfolding invertible_det_nz[symmetric] invertible_def
   1.454      by blast
   1.455 @@ -941,14 +941,14 @@
   1.456      by auto
   1.457  qed
   1.458  
   1.459 -subsection \<open>Orthogonality of a transformation and matrix\<close>
   1.460 +subsection%important  \<open>Orthogonality of a transformation and matrix\<close>
   1.461  
   1.462 -definition "orthogonal_transformation f \<longleftrightarrow> linear f \<and> (\<forall>v w. f v \<bullet> f w = v \<bullet> w)"
   1.463 +definition%important  "orthogonal_transformation f \<longleftrightarrow> linear f \<and> (\<forall>v w. f v \<bullet> f w = v \<bullet> w)"
   1.464  
   1.465 -definition "orthogonal_matrix (Q::'a::semiring_1^'n^'n) \<longleftrightarrow>
   1.466 +definition%important  "orthogonal_matrix (Q::'a::semiring_1^'n^'n) \<longleftrightarrow>
   1.467    transpose Q ** Q = mat 1 \<and> Q ** transpose Q = mat 1"
   1.468  
   1.469 -lemma orthogonal_transformation:
   1.470 +lemma%unimportant  orthogonal_transformation:
   1.471    "orthogonal_transformation f \<longleftrightarrow> linear f \<and> (\<forall>v. norm (f v) = norm v)"
   1.472    unfolding orthogonal_transformation_def
   1.473    apply auto
   1.474 @@ -957,70 +957,70 @@
   1.475    apply (simp add: dot_norm linear_add[symmetric])
   1.476    done
   1.477  
   1.478 -lemma orthogonal_transformation_id [simp]: "orthogonal_transformation (\<lambda>x. x)"
   1.479 +lemma%unimportant  orthogonal_transformation_id [simp]: "orthogonal_transformation (\<lambda>x. x)"
   1.480    by (simp add: linear_iff orthogonal_transformation_def)
   1.481  
   1.482 -lemma orthogonal_orthogonal_transformation:
   1.483 +lemma%unimportant  orthogonal_orthogonal_transformation:
   1.484      "orthogonal_transformation f \<Longrightarrow> orthogonal (f x) (f y) \<longleftrightarrow> orthogonal x y"
   1.485    by (simp add: orthogonal_def orthogonal_transformation_def)
   1.486  
   1.487 -lemma orthogonal_transformation_compose:
   1.488 +lemma%unimportant  orthogonal_transformation_compose:
   1.489     "\<lbrakk>orthogonal_transformation f; orthogonal_transformation g\<rbrakk> \<Longrightarrow> orthogonal_transformation(f \<circ> g)"
   1.490    by (auto simp: orthogonal_transformation_def linear_compose)
   1.491  
   1.492 -lemma orthogonal_transformation_neg:
   1.493 +lemma%unimportant  orthogonal_transformation_neg:
   1.494    "orthogonal_transformation(\<lambda>x. -(f x)) \<longleftrightarrow> orthogonal_transformation f"
   1.495    by (auto simp: orthogonal_transformation_def dest: linear_compose_neg)
   1.496  
   1.497 -lemma orthogonal_transformation_scaleR: "orthogonal_transformation f \<Longrightarrow> f (c *\<^sub>R v) = c *\<^sub>R f v"
   1.498 +lemma%unimportant  orthogonal_transformation_scaleR: "orthogonal_transformation f \<Longrightarrow> f (c *\<^sub>R v) = c *\<^sub>R f v"
   1.499    by (simp add: linear_iff orthogonal_transformation_def)
   1.500  
   1.501 -lemma orthogonal_transformation_linear:
   1.502 +lemma%unimportant  orthogonal_transformation_linear:
   1.503     "orthogonal_transformation f \<Longrightarrow> linear f"
   1.504    by (simp add: orthogonal_transformation_def)
   1.505  
   1.506 -lemma orthogonal_transformation_inj:
   1.507 +lemma%unimportant  orthogonal_transformation_inj:
   1.508    "orthogonal_transformation f \<Longrightarrow> inj f"
   1.509    unfolding orthogonal_transformation_def inj_on_def
   1.510    by (metis vector_eq)
   1.511  
   1.512 -lemma orthogonal_transformation_surj:
   1.513 +lemma%unimportant  orthogonal_transformation_surj:
   1.514    "orthogonal_transformation f \<Longrightarrow> surj f"
   1.515    for f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
   1.516    by (simp add: linear_injective_imp_surjective orthogonal_transformation_inj orthogonal_transformation_linear)
   1.517  
   1.518 -lemma orthogonal_transformation_bij:
   1.519 +lemma%unimportant  orthogonal_transformation_bij:
   1.520    "orthogonal_transformation f \<Longrightarrow> bij f"
   1.521    for f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
   1.522    by (simp add: bij_def orthogonal_transformation_inj orthogonal_transformation_surj)
   1.523  
   1.524 -lemma orthogonal_transformation_inv:
   1.525 +lemma%unimportant  orthogonal_transformation_inv:
   1.526    "orthogonal_transformation f \<Longrightarrow> orthogonal_transformation (inv f)"
   1.527    for f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
   1.528    by (metis (no_types, hide_lams) bijection.inv_right bijection_def inj_linear_imp_inv_linear orthogonal_transformation orthogonal_transformation_bij orthogonal_transformation_inj)
   1.529  
   1.530 -lemma orthogonal_transformation_norm:
   1.531 +lemma%unimportant  orthogonal_transformation_norm:
   1.532    "orthogonal_transformation f \<Longrightarrow> norm (f x) = norm x"
   1.533    by (metis orthogonal_transformation)
   1.534  
   1.535 -lemma orthogonal_matrix: "orthogonal_matrix (Q:: real ^'n^'n) \<longleftrightarrow> transpose Q ** Q = mat 1"
   1.536 +lemma%unimportant  orthogonal_matrix: "orthogonal_matrix (Q:: real ^'n^'n) \<longleftrightarrow> transpose Q ** Q = mat 1"
   1.537    by (metis matrix_left_right_inverse orthogonal_matrix_def)
   1.538  
   1.539 -lemma orthogonal_matrix_id: "orthogonal_matrix (mat 1 :: _^'n^'n)"
   1.540 +lemma%unimportant  orthogonal_matrix_id: "orthogonal_matrix (mat 1 :: _^'n^'n)"
   1.541    by (simp add: orthogonal_matrix_def)
   1.542  
   1.543 -lemma orthogonal_matrix_mul:
   1.544 +lemma%unimportant  orthogonal_matrix_mul:
   1.545    fixes A :: "real ^'n^'n"
   1.546    assumes  "orthogonal_matrix A" "orthogonal_matrix B"
   1.547    shows "orthogonal_matrix(A ** B)"
   1.548    using assms
   1.549    by (simp add: orthogonal_matrix matrix_transpose_mul matrix_left_right_inverse matrix_mul_assoc)
   1.550  
   1.551 -lemma orthogonal_transformation_matrix:
   1.552 +lemma%important  orthogonal_transformation_matrix:
   1.553    fixes f:: "real^'n \<Rightarrow> real^'n"
   1.554    shows "orthogonal_transformation f \<longleftrightarrow> linear f \<and> orthogonal_matrix(matrix f)"
   1.555    (is "?lhs \<longleftrightarrow> ?rhs")
   1.556 -proof -
   1.557 +proof%unimportant -
   1.558    let ?mf = "matrix f"
   1.559    let ?ot = "orthogonal_transformation f"
   1.560    let ?U = "UNIV :: 'n set"
   1.561 @@ -1063,11 +1063,11 @@
   1.562      by (auto simp: linear_def scalar_mult_eq_scaleR)
   1.563  qed
   1.564  
   1.565 -lemma det_orthogonal_matrix:
   1.566 +lemma%important  det_orthogonal_matrix:
   1.567    fixes Q:: "'a::linordered_idom^'n^'n"
   1.568    assumes oQ: "orthogonal_matrix Q"
   1.569    shows "det Q = 1 \<or> det Q = - 1"
   1.570 -proof -
   1.571 +proof%unimportant -
   1.572    have "Q ** transpose Q = mat 1"
   1.573      by (metis oQ orthogonal_matrix_def)
   1.574    then have "det (Q ** transpose Q) = det (mat 1:: 'a^'n^'n)"
   1.575 @@ -1078,20 +1078,20 @@
   1.576      by (simp add: square_eq_1_iff)
   1.577  qed
   1.578  
   1.579 -lemma orthogonal_transformation_det [simp]:
   1.580 +lemma%important  orthogonal_transformation_det [simp]:
   1.581    fixes f :: "real^'n \<Rightarrow> real^'n"
   1.582    shows "orthogonal_transformation f \<Longrightarrow> \<bar>det (matrix f)\<bar> = 1"
   1.583 -  using det_orthogonal_matrix orthogonal_transformation_matrix by fastforce
   1.584 +  using%unimportant det_orthogonal_matrix orthogonal_transformation_matrix by fastforce
   1.585  
   1.586  
   1.587 -subsection \<open>Linearity of scaling, and hence isometry, that preserves origin\<close>
   1.588 +subsection%important  \<open>Linearity of scaling, and hence isometry, that preserves origin\<close>
   1.589  
   1.590 -lemma scaling_linear:
   1.591 +lemma%important  scaling_linear:
   1.592    fixes f :: "'a::real_inner \<Rightarrow> 'a::real_inner"
   1.593    assumes f0: "f 0 = 0"
   1.594      and fd: "\<forall>x y. dist (f x) (f y) = c * dist x y"
   1.595    shows "linear f"
   1.596 -proof -
   1.597 +proof%unimportant -
   1.598    {
   1.599      fix v w
   1.600      have "norm (f x) = c * norm x" for x
   1.601 @@ -1105,13 +1105,13 @@
   1.602      by (simp add: inner_add field_simps)
   1.603  qed
   1.604  
   1.605 -lemma isometry_linear:
   1.606 +lemma%unimportant  isometry_linear:
   1.607    "f (0::'a::real_inner) = (0::'a) \<Longrightarrow> \<forall>x y. dist(f x) (f y) = dist x y \<Longrightarrow> linear f"
   1.608    by (rule scaling_linear[where c=1]) simp_all
   1.609  
   1.610  text \<open>Hence another formulation of orthogonal transformation\<close>
   1.611  
   1.612 -lemma orthogonal_transformation_isometry:
   1.613 +lemma%important  orthogonal_transformation_isometry:
   1.614    "orthogonal_transformation f \<longleftrightarrow> f(0::'a::real_inner) = (0::'a) \<and> (\<forall>x y. dist(f x) (f y) = dist x y)"
   1.615    unfolding orthogonal_transformation
   1.616    apply (auto simp: linear_0 isometry_linear)
   1.617 @@ -1119,7 +1119,7 @@
   1.618    by (metis dist_0_norm)
   1.619  
   1.620  
   1.621 -lemma image_orthogonal_transformation_ball:
   1.622 +lemma%unimportant  image_orthogonal_transformation_ball:
   1.623    fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
   1.624    assumes "orthogonal_transformation f"
   1.625    shows "f ` ball x r = ball (f x) r"
   1.626 @@ -1135,7 +1135,7 @@
   1.627      by (auto simp: orthogonal_transformation_isometry)
   1.628  qed
   1.629  
   1.630 -lemma image_orthogonal_transformation_cball:
   1.631 +lemma%unimportant  image_orthogonal_transformation_cball:
   1.632    fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
   1.633    assumes "orthogonal_transformation f"
   1.634    shows "f ` cball x r = cball (f x) r"
   1.635 @@ -1151,31 +1151,31 @@
   1.636      by (auto simp: orthogonal_transformation_isometry)
   1.637  qed
   1.638  
   1.639 -subsection\<open> We can find an orthogonal matrix taking any unit vector to any other\<close>
   1.640 +subsection%important \<open> We can find an orthogonal matrix taking any unit vector to any other\<close>
   1.641  
   1.642 -lemma orthogonal_matrix_transpose [simp]:
   1.643 +lemma%unimportant  orthogonal_matrix_transpose [simp]:
   1.644       "orthogonal_matrix(transpose A) \<longleftrightarrow> orthogonal_matrix A"
   1.645    by (auto simp: orthogonal_matrix_def)
   1.646  
   1.647 -lemma orthogonal_matrix_orthonormal_columns:
   1.648 +lemma%unimportant  orthogonal_matrix_orthonormal_columns:
   1.649    fixes A :: "real^'n^'n"
   1.650    shows "orthogonal_matrix A \<longleftrightarrow>
   1.651            (\<forall>i. norm(column i A) = 1) \<and>
   1.652            (\<forall>i j. i \<noteq> j \<longrightarrow> orthogonal (column i A) (column j A))"
   1.653    by (auto simp: orthogonal_matrix matrix_mult_transpose_dot_column vec_eq_iff mat_def norm_eq_1 orthogonal_def)
   1.654  
   1.655 -lemma orthogonal_matrix_orthonormal_rows:
   1.656 +lemma%unimportant  orthogonal_matrix_orthonormal_rows:
   1.657    fixes A :: "real^'n^'n"
   1.658    shows "orthogonal_matrix A \<longleftrightarrow>
   1.659            (\<forall>i. norm(row i A) = 1) \<and>
   1.660            (\<forall>i j. i \<noteq> j \<longrightarrow> orthogonal (row i A) (row j A))"
   1.661    using orthogonal_matrix_orthonormal_columns [of "transpose A"] by simp
   1.662  
   1.663 -lemma orthogonal_matrix_exists_basis:
   1.664 +lemma%important  orthogonal_matrix_exists_basis:
   1.665    fixes a :: "real^'n"
   1.666    assumes "norm a = 1"
   1.667    obtains A where "orthogonal_matrix A" "A *v (axis k 1) = a"
   1.668 -proof -
   1.669 +proof%unimportant -
   1.670    obtain S where "a \<in> S" "pairwise orthogonal S" and noS: "\<And>x. x \<in> S \<Longrightarrow> norm x = 1"
   1.671     and "independent S" "card S = CARD('n)" "span S = UNIV"
   1.672      using vector_in_orthonormal_basis assms by force
   1.673 @@ -1198,11 +1198,11 @@
   1.674    qed
   1.675  qed
   1.676  
   1.677 -lemma orthogonal_transformation_exists_1:
   1.678 +lemma%unimportant  orthogonal_transformation_exists_1:
   1.679    fixes a b :: "real^'n"
   1.680    assumes "norm a = 1" "norm b = 1"
   1.681    obtains f where "orthogonal_transformation f" "f a = b"
   1.682 -proof -
   1.683 +proof%unimportant -
   1.684    obtain k::'n where True
   1.685      by simp
   1.686    obtain A B where AB: "orthogonal_matrix A" "orthogonal_matrix B" and eq: "A *v (axis k 1) = a" "B *v (axis k 1) = b"
   1.687 @@ -1220,11 +1220,11 @@
   1.688    qed
   1.689  qed
   1.690  
   1.691 -lemma orthogonal_transformation_exists:
   1.692 +lemma%important  orthogonal_transformation_exists:
   1.693    fixes a b :: "real^'n"
   1.694    assumes "norm a = norm b"
   1.695    obtains f where "orthogonal_transformation f" "f a = b"
   1.696 -proof (cases "a = 0 \<or> b = 0")
   1.697 +proof%unimportant (cases "a = 0 \<or> b = 0")
   1.698    case True
   1.699    with assms show ?thesis
   1.700      using that by force
   1.701 @@ -1246,14 +1246,14 @@
   1.702  qed
   1.703  
   1.704  
   1.705 -subsection \<open>Can extend an isometry from unit sphere\<close>
   1.706 +subsection%important  \<open>Can extend an isometry from unit sphere\<close>
   1.707  
   1.708 -lemma isometry_sphere_extend:
   1.709 +lemma%important  isometry_sphere_extend:
   1.710    fixes f:: "'a::real_inner \<Rightarrow> 'a"
   1.711    assumes f1: "\<And>x. norm x = 1 \<Longrightarrow> norm (f x) = 1"
   1.712      and fd1: "\<And>x y. \<lbrakk>norm x = 1; norm y = 1\<rbrakk> \<Longrightarrow> dist (f x) (f y) = dist x y"
   1.713    shows "\<exists>g. orthogonal_transformation g \<and> (\<forall>x. norm x = 1 \<longrightarrow> g x = f x)"
   1.714 -proof -
   1.715 +proof%unimportant -
   1.716    {
   1.717      fix x y x' y' u v u' v' :: "'a"
   1.718      assume H: "x = norm x *\<^sub>R u" "y = norm y *\<^sub>R v"
   1.719 @@ -1286,31 +1286,31 @@
   1.720      by (rule exI[where x= ?g]) (metis thfg thd)
   1.721  qed
   1.722  
   1.723 -subsection \<open>Rotation, reflection, rotoinversion\<close>
   1.724 +subsection%important  \<open>Rotation, reflection, rotoinversion\<close>
   1.725  
   1.726 -definition "rotation_matrix Q \<longleftrightarrow> orthogonal_matrix Q \<and> det Q = 1"
   1.727 -definition "rotoinversion_matrix Q \<longleftrightarrow> orthogonal_matrix Q \<and> det Q = - 1"
   1.728 +definition%important  "rotation_matrix Q \<longleftrightarrow> orthogonal_matrix Q \<and> det Q = 1"
   1.729 +definition%important  "rotoinversion_matrix Q \<longleftrightarrow> orthogonal_matrix Q \<and> det Q = - 1"
   1.730  
   1.731 -lemma orthogonal_rotation_or_rotoinversion:
   1.732 +lemma%important  orthogonal_rotation_or_rotoinversion:
   1.733    fixes Q :: "'a::linordered_idom^'n^'n"
   1.734    shows " orthogonal_matrix Q \<longleftrightarrow> rotation_matrix Q \<or> rotoinversion_matrix Q"
   1.735 -  by (metis rotoinversion_matrix_def rotation_matrix_def det_orthogonal_matrix)
   1.736 +  by%unimportant (metis rotoinversion_matrix_def rotation_matrix_def det_orthogonal_matrix)
   1.737  
   1.738  text \<open>Explicit formulas for low dimensions\<close>
   1.739  
   1.740 -lemma prod_neutral_const: "prod f {(1::nat)..1} = f 1"
   1.741 +lemma%unimportant  prod_neutral_const: "prod f {(1::nat)..1} = f 1"
   1.742    by simp
   1.743  
   1.744 -lemma prod_2: "prod f {(1::nat)..2} = f 1 * f 2"
   1.745 +lemma%unimportant  prod_2: "prod f {(1::nat)..2} = f 1 * f 2"
   1.746    by (simp add: eval_nat_numeral atLeastAtMostSuc_conv mult.commute)
   1.747  
   1.748 -lemma prod_3: "prod f {(1::nat)..3} = f 1 * f 2 * f 3"
   1.749 +lemma%unimportant  prod_3: "prod f {(1::nat)..3} = f 1 * f 2 * f 3"
   1.750    by (simp add: eval_nat_numeral atLeastAtMostSuc_conv mult.commute)
   1.751  
   1.752 -lemma det_1: "det (A::'a::comm_ring_1^1^1) = A$1$1"
   1.753 +lemma%unimportant  det_1: "det (A::'a::comm_ring_1^1^1) = A$1$1"
   1.754    by (simp add: det_def sign_id)
   1.755  
   1.756 -lemma det_2: "det (A::'a::comm_ring_1^2^2) = A$1$1 * A$2$2 - A$1$2 * A$2$1"
   1.757 +lemma%unimportant  det_2: "det (A::'a::comm_ring_1^2^2) = A$1$1 * A$2$2 - A$1$2 * A$2$1"
   1.758  proof -
   1.759    have f12: "finite {2::2}" "1 \<notin> {2::2}" by auto
   1.760    show ?thesis
   1.761 @@ -1320,7 +1320,7 @@
   1.762      by (simp add: sign_swap_id sign_id swap_id_eq)
   1.763  qed
   1.764  
   1.765 -lemma det_3:
   1.766 +lemma%unimportant  det_3:
   1.767    "det (A::'a::comm_ring_1^3^3) =
   1.768      A$1$1 * A$2$2 * A$3$3 +
   1.769      A$1$2 * A$2$3 * A$3$1 +
   1.770 @@ -1344,7 +1344,7 @@
   1.771  
   1.772  text\<open> Slightly stronger results giving rotation, but only in two or more dimensions\<close>
   1.773  
   1.774 -lemma rotation_matrix_exists_basis:
   1.775 +lemma%unimportant  rotation_matrix_exists_basis:
   1.776    fixes a :: "real^'n"
   1.777    assumes 2: "2 \<le> CARD('n)" and "norm a = 1"
   1.778    obtains A where "rotation_matrix A" "A *v (axis k 1) = a"
   1.779 @@ -1383,7 +1383,7 @@
   1.780    qed
   1.781  qed
   1.782  
   1.783 -lemma rotation_exists_1:
   1.784 +lemma%unimportant  rotation_exists_1:
   1.785    fixes a :: "real^'n"
   1.786    assumes "2 \<le> CARD('n)" "norm a = 1" "norm b = 1"
   1.787    obtains f where "orthogonal_transformation f" "det(matrix f) = 1" "f a = b"
   1.788 @@ -1406,7 +1406,7 @@
   1.789    qed
   1.790  qed
   1.791  
   1.792 -lemma rotation_exists:
   1.793 +lemma%unimportant  rotation_exists:
   1.794    fixes a :: "real^'n"
   1.795    assumes 2: "2 \<le> CARD('n)" and eq: "norm a = norm b"
   1.796    obtains f where "orthogonal_transformation f" "det(matrix f) = 1" "f a = b"
   1.797 @@ -1428,7 +1428,7 @@
   1.798    with f show thesis ..
   1.799  qed
   1.800  
   1.801 -lemma rotation_rightward_line:
   1.802 +lemma%unimportant  rotation_rightward_line:
   1.803    fixes a :: "real^'n"
   1.804    obtains f where "orthogonal_transformation f" "2 \<le> CARD('n) \<Longrightarrow> det(matrix f) = 1"
   1.805                    "f(norm a *\<^sub>R axis k 1) = a"