equal
deleted
inserted
replaced
462 apply blast |
462 apply blast |
463 apply (rule x) |
463 apply (rule x) |
464 done |
464 done |
465 qed |
465 qed |
466 |
466 |
467 lemma matrix_id_mat_1: "matrix id = mat 1" |
|
468 by (simp add: mat_def matrix_def axis_def) |
|
469 |
|
470 lemma matrix_id [simp]: "det (matrix id) = 1" |
467 lemma matrix_id [simp]: "det (matrix id) = 1" |
471 by (simp add: matrix_id_mat_1) |
468 by (simp add: matrix_id_mat_1) |
472 |
|
473 lemma matrix_scaleR: "(matrix (( *\<^sub>R) r)) = mat r" |
|
474 by (simp add: mat_def matrix_def axis_def if_distrib cong: if_cong) |
|
475 |
469 |
476 lemma det_matrix_scaleR [simp]: "det (matrix ((( *\<^sub>R) r)) :: real^'n^'n) = r ^ CARD('n::finite)" |
470 lemma det_matrix_scaleR [simp]: "det (matrix ((( *\<^sub>R) r)) :: real^'n^'n) = r ^ CARD('n::finite)" |
477 apply (subst det_diagonal) |
471 apply (subst det_diagonal) |
478 apply (auto simp: matrix_def mat_def prod_constant) |
472 apply (auto simp: matrix_def mat_def prod_constant) |
479 apply (simp add: cart_eq_inner_axis inner_axis_axis) |
473 apply (simp add: cart_eq_inner_axis inner_axis_axis) |