equal
deleted
inserted
replaced
1540 instance matrix :: (group_add) group_add |
1540 instance matrix :: (group_add) group_add |
1541 proof |
1541 proof |
1542 fix A B :: "'a matrix" |
1542 fix A B :: "'a matrix" |
1543 show "- A + A = 0" |
1543 show "- A + A = 0" |
1544 by (simp add: plus_matrix_def minus_matrix_def Rep_matrix_inject[symmetric] ext) |
1544 by (simp add: plus_matrix_def minus_matrix_def Rep_matrix_inject[symmetric] ext) |
1545 show "A - B = A + - B" |
1545 show "A + - B = A - B" |
1546 by (simp add: plus_matrix_def diff_matrix_def minus_matrix_def Rep_matrix_inject [symmetric] ext diff_minus) |
1546 by (simp add: plus_matrix_def diff_matrix_def minus_matrix_def Rep_matrix_inject [symmetric] ext) |
1547 qed |
1547 qed |
1548 |
1548 |
1549 instance matrix :: (ab_group_add) ab_group_add |
1549 instance matrix :: (ab_group_add) ab_group_add |
1550 proof |
1550 proof |
1551 fix A B :: "'a matrix" |
1551 fix A B :: "'a matrix" |