1661 apply (subst Rep_matrix_inject[THEN sym]) |
1661 apply (subst Rep_matrix_inject[THEN sym]) |
1662 apply (rule ext)+ |
1662 apply (rule ext)+ |
1663 apply (simp add: times_matrix_def Rep_mult_matrix) |
1663 apply (simp add: times_matrix_def Rep_mult_matrix) |
1664 apply (rule_tac j1="xa" in ssubst[OF foldseq_almostzero]) |
1664 apply (rule_tac j1="xa" in ssubst[OF foldseq_almostzero]) |
1665 apply (simp_all) |
1665 apply (simp_all) |
1666 by (simp add: max_def ncols) |
1666 by (simp add: ncols) |
1667 |
1667 |
1668 lemma one_matrix_mult_left[simp]: "nrows A <= n \<Longrightarrow> (one_matrix n) * A = (A::('a::ring_1) matrix)" |
1668 lemma one_matrix_mult_left[simp]: "nrows A <= n \<Longrightarrow> (one_matrix n) * A = (A::('a::ring_1) matrix)" |
1669 apply (subst Rep_matrix_inject[THEN sym]) |
1669 apply (subst Rep_matrix_inject[THEN sym]) |
1670 apply (rule ext)+ |
1670 apply (rule ext)+ |
1671 apply (simp add: times_matrix_def Rep_mult_matrix) |
1671 apply (simp add: times_matrix_def Rep_mult_matrix) |
1672 apply (rule_tac j1="x" in ssubst[OF foldseq_almostzero]) |
1672 apply (rule_tac j1="x" in ssubst[OF foldseq_almostzero]) |
1673 apply (simp_all) |
1673 apply (simp_all) |
1674 by (simp add: max_def nrows) |
1674 by (simp add: nrows) |
1675 |
1675 |
1676 lemma transpose_matrix_mult: "transpose_matrix ((A::('a::comm_ring) matrix)*B) = (transpose_matrix B) * (transpose_matrix A)" |
1676 lemma transpose_matrix_mult: "transpose_matrix ((A::('a::comm_ring) matrix)*B) = (transpose_matrix B) * (transpose_matrix A)" |
1677 apply (simp add: times_matrix_def) |
1677 apply (simp add: times_matrix_def) |
1678 apply (subst transpose_mult_matrix) |
1678 apply (subst transpose_mult_matrix) |
1679 apply (simp_all add: mult_commute) |
1679 apply (simp_all add: mult_commute) |