[STATEMENT]
lemma Gram_Schmidt_column_k_code[code abstract]:
  "vec_nth (Gram_Schmidt_column_k A k) = Gram_Schmidt_column_k_row A k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ($) (Gram_Schmidt_column_k A k) = Gram_Schmidt_column_k_row A k
[PROOF STEP]
unfolding Gram_Schmidt_column_k_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ($) (\<chi>a b. (if b = mod_type_class.from_nat k then column b A - proj_onto (column b A) {column i A |i. i < b} else column b A) $ a) = Gram_Schmidt_column_k_row A k
[PROOF STEP]
unfolding Gram_Schmidt_column_k_row_def[abs_def]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ($) (\<chi>a b. (if b = mod_type_class.from_nat k then column b A - proj_onto (column b A) {column i A |i. i < b} else column b A) $ a) = (\<lambda>a. \<chi>b. (if b = mod_type_class.from_nat k then column b A - (\<Sum>x\<in>{column i A |i. i < b}. (column b A \<bullet> x / (x \<bullet> x)) *\<^sub>R x) else column b A) $ a)
[PROOF STEP]
unfolding proj_onto_def proj_def[abs_def]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ($) (\<chi>a b. (if b = mod_type_class.from_nat k then column b A - (\<Sum>u\<in>{column i A |i. i < b}. (column b A \<bullet> u / (u \<bullet> u)) *\<^sub>R u) else column b A) $ a) = (\<lambda>a. \<chi>b. (if b = mod_type_class.from_nat k then column b A - (\<Sum>x\<in>{column i A |i. i < b}. (column b A \<bullet> x / (x \<bullet> x)) *\<^sub>R x) else column b A) $ a)
[PROOF STEP]
by fastforce