src/HOL/Analysis/Cartesian_Euclidean_Space.thy
changeset 68077 ee8c13ae81e9
parent 68074 8d50467f7555
child 68833 fde093888c16
     1.1 --- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Thu May 03 18:40:14 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Thu May 03 22:34:49 2018 +0100
     1.3 @@ -939,15 +939,16 @@
     1.4    fixes A :: "real^'n^'m"
     1.5    assumes 0: "A *v x = 0" and y: "y \<in> span(rows A)"
     1.6    shows "orthogonal x y"
     1.7 -proof (rule span_induct [OF y])
     1.8 -  show "subspace {a. orthogonal x a}"
     1.9 +  using y
    1.10 +proof (induction rule: span_induct)
    1.11 +  case base
    1.12 +  then show ?case
    1.13      by (simp add: subspace_orthogonal_to_vector)
    1.14  next
    1.15 -  fix v
    1.16 -  assume "v \<in> rows A"
    1.17 +  case (step v)
    1.18    then obtain i where "v = row i A"
    1.19      by (auto simp: rows_def)
    1.20 -  with 0 show "orthogonal x v"
    1.21 +  with 0 show ?case
    1.22      unfolding orthogonal_def inner_vec_def matrix_vector_mult_def row_def
    1.23      by (simp add: mult.commute) (metis (no_types) vec_lambda_beta zero_index)
    1.24  qed