1487 |
1487 |
1488 instance .. |
1488 instance .. |
1489 |
1489 |
1490 end |
1490 end |
1491 |
1491 |
1492 instantiation matrix :: (lordered_ab_group_add) abs |
1492 instantiation matrix :: ("{lattice, uminus, zero}") abs |
1493 begin |
1493 begin |
1494 |
1494 |
1495 definition |
1495 definition |
1496 abs_matrix_def [code func del]: "abs (A \<Colon> 'a matrix) = sup A (- A)" |
1496 abs_matrix_def [code func del]: "abs (A \<Colon> 'a matrix) = sup A (- A)" |
1497 |
1497 |
1498 instance .. |
1498 instance .. |
1499 |
1499 |
1500 end |
1500 end |
1501 |
1501 |
1502 instance matrix :: (lordered_ab_group_add) lordered_ab_group_add_meet |
1502 instance matrix :: (monoid_add) monoid_add |
1503 proof |
1503 proof |
1504 fix A B C :: "('a::lordered_ab_group_add) matrix" |
1504 fix A B C :: "'a matrix" |
1505 show "A + B + C = A + (B + C)" |
1505 show "A + B + C = A + (B + C)" |
1506 apply (simp add: plus_matrix_def) |
1506 apply (simp add: plus_matrix_def) |
1507 apply (rule combine_matrix_assoc[simplified associative_def, THEN spec, THEN spec, THEN spec]) |
1507 apply (rule combine_matrix_assoc[simplified associative_def, THEN spec, THEN spec, THEN spec]) |
1508 apply (simp_all add: add_assoc) |
1508 apply (simp_all add: add_assoc) |
1509 done |
1509 done |
|
1510 show "0 + A = A" |
|
1511 apply (simp add: plus_matrix_def) |
|
1512 apply (rule combine_matrix_zero_l_neutral[simplified zero_l_neutral_def, THEN spec]) |
|
1513 apply (simp) |
|
1514 done |
|
1515 show "A + 0 = A" |
|
1516 apply (simp add: plus_matrix_def) |
|
1517 apply (rule combine_matrix_zero_r_neutral [simplified zero_r_neutral_def, THEN spec]) |
|
1518 apply (simp) |
|
1519 done |
|
1520 qed |
|
1521 |
|
1522 instance matrix :: (comm_monoid_add) comm_monoid_add |
|
1523 proof |
|
1524 fix A B :: "'a matrix" |
1510 show "A + B = B + A" |
1525 show "A + B = B + A" |
1511 apply (simp add: plus_matrix_def) |
1526 apply (simp add: plus_matrix_def) |
1512 apply (rule combine_matrix_commute[simplified commutative_def, THEN spec, THEN spec]) |
1527 apply (rule combine_matrix_commute[simplified commutative_def, THEN spec, THEN spec]) |
1513 apply (simp_all add: add_commute) |
1528 apply (simp_all add: add_commute) |
1514 done |
1529 done |
1515 show "0 + A = A" |
1530 show "0 + A = A" |
1516 apply (simp add: plus_matrix_def) |
1531 apply (simp add: plus_matrix_def) |
1517 apply (rule combine_matrix_zero_l_neutral[simplified zero_l_neutral_def, THEN spec]) |
1532 apply (rule combine_matrix_zero_l_neutral[simplified zero_l_neutral_def, THEN spec]) |
1518 apply (simp) |
1533 apply (simp) |
1519 done |
1534 done |
|
1535 qed |
|
1536 |
|
1537 instance matrix :: (group_add) group_add |
|
1538 proof |
|
1539 fix A B :: "'a matrix" |
|
1540 show "- A + A = 0" |
|
1541 by (simp add: plus_matrix_def minus_matrix_def Rep_matrix_inject[symmetric] ext) |
|
1542 show "A - B = A + - B" |
|
1543 by (simp add: plus_matrix_def diff_matrix_def minus_matrix_def Rep_matrix_inject [symmetric] ext diff_minus) |
|
1544 qed |
|
1545 |
|
1546 instance matrix :: (ab_group_add) ab_group_add |
|
1547 proof |
|
1548 fix A B :: "'a matrix" |
1520 show "- A + A = 0" |
1549 show "- A + A = 0" |
1521 by (simp add: plus_matrix_def minus_matrix_def Rep_matrix_inject[symmetric] ext) |
1550 by (simp add: plus_matrix_def minus_matrix_def Rep_matrix_inject[symmetric] ext) |
1522 show "A - B = A + - B" |
1551 show "A - B = A + - B" |
1523 by (simp add: plus_matrix_def diff_matrix_def minus_matrix_def Rep_matrix_inject[symmetric] ext) |
1552 by (simp add: plus_matrix_def diff_matrix_def minus_matrix_def Rep_matrix_inject[symmetric] ext) |
|
1553 qed |
|
1554 |
|
1555 instance matrix :: (pordered_ab_group_add) pordered_ab_group_add |
|
1556 proof |
|
1557 fix A B C :: "'a matrix" |
1524 assume "A <= B" |
1558 assume "A <= B" |
1525 then show "C + A <= C + B" |
1559 then show "C + A <= C + B" |
1526 apply (simp add: plus_matrix_def) |
1560 apply (simp add: plus_matrix_def) |
1527 apply (rule le_left_combine_matrix) |
1561 apply (rule le_left_combine_matrix) |
1528 apply (simp_all) |
1562 apply (simp_all) |
1529 done |
1563 done |
1530 qed |
1564 qed |
1531 |
1565 |
1532 instance matrix :: (lordered_ring) lordered_ring |
1566 instance matrix :: (lordered_ab_group_add) lordered_ab_group_add_meet .. |
|
1567 instance matrix :: (lordered_ab_group_add) lordered_ab_group_add_join .. |
|
1568 |
|
1569 instance matrix :: (ring) ring |
1533 proof |
1570 proof |
1534 fix A B C :: "('a :: lordered_ring) matrix" |
1571 fix A B C :: "'a matrix" |
1535 show "A * B * C = A * (B * C)" |
1572 show "A * B * C = A * (B * C)" |
1536 apply (simp add: times_matrix_def) |
1573 apply (simp add: times_matrix_def) |
1537 apply (rule mult_matrix_assoc) |
1574 apply (rule mult_matrix_assoc) |
1538 apply (simp_all add: associative_def ring_simps) |
1575 apply (simp_all add: associative_def ring_simps) |
1539 done |
1576 done |
1544 done |
1581 done |
1545 show "A * (B + C) = A * B + A * C" |
1582 show "A * (B + C) = A * B + A * C" |
1546 apply (simp add: times_matrix_def plus_matrix_def) |
1583 apply (simp add: times_matrix_def plus_matrix_def) |
1547 apply (rule r_distributive_matrix[simplified r_distributive_def, THEN spec, THEN spec, THEN spec]) |
1584 apply (rule r_distributive_matrix[simplified r_distributive_def, THEN spec, THEN spec, THEN spec]) |
1548 apply (simp_all add: associative_def commutative_def ring_simps) |
1585 apply (simp_all add: associative_def commutative_def ring_simps) |
1549 done |
1586 done |
1550 show "abs A = sup A (-A)" |
1587 qed |
1551 by (simp add: abs_matrix_def) |
1588 |
|
1589 instance matrix :: (pordered_ring) pordered_ring |
|
1590 proof |
|
1591 fix A B C :: "'a matrix" |
1552 assume a: "A \<le> B" |
1592 assume a: "A \<le> B" |
1553 assume b: "0 \<le> C" |
1593 assume b: "0 \<le> C" |
1554 from a b show "C * A \<le> C * B" |
1594 from a b show "C * A \<le> C * B" |
1555 apply (simp add: times_matrix_def) |
1595 apply (simp add: times_matrix_def) |
1556 apply (rule le_left_mult) |
1596 apply (rule le_left_mult) |
1559 from a b show "A * C \<le> B * C" |
1599 from a b show "A * C \<le> B * C" |
1560 apply (simp add: times_matrix_def) |
1600 apply (simp add: times_matrix_def) |
1561 apply (rule le_right_mult) |
1601 apply (rule le_right_mult) |
1562 apply (simp_all add: add_mono mult_right_mono) |
1602 apply (simp_all add: add_mono mult_right_mono) |
1563 done |
1603 done |
1564 qed |
1604 qed |
|
1605 |
|
1606 instance matrix :: (lordered_ring) lordered_ring |
|
1607 proof |
|
1608 fix A B C :: "('a :: lordered_ring) matrix" |
|
1609 show "abs A = sup A (-A)" |
|
1610 by (simp add: abs_matrix_def) |
|
1611 qed |
1565 |
1612 |
1566 lemma Rep_matrix_add[simp]: |
1613 lemma Rep_matrix_add[simp]: |
1567 "Rep_matrix ((a::('a::lordered_ab_group_add)matrix)+b) j i = (Rep_matrix a j i) + (Rep_matrix b j i)" |
1614 "Rep_matrix ((a::('a::monoid_add)matrix)+b) j i = (Rep_matrix a j i) + (Rep_matrix b j i)" |
1568 by (simp add: plus_matrix_def) |
1615 by (simp add: plus_matrix_def) |
1569 |
1616 |
1570 lemma Rep_matrix_mult: "Rep_matrix ((a::('a::lordered_ring) matrix) * b) j i = |
1617 lemma Rep_matrix_mult: "Rep_matrix ((a::('a::ring) matrix) * b) j i = |
1571 foldseq (op +) (% k. (Rep_matrix a j k) * (Rep_matrix b k i)) (max (ncols a) (nrows b))" |
1618 foldseq (op +) (% k. (Rep_matrix a j k) * (Rep_matrix b k i)) (max (ncols a) (nrows b))" |
1572 apply (simp add: times_matrix_def) |
1619 apply (simp add: times_matrix_def) |
1573 apply (simp add: Rep_mult_matrix) |
1620 apply (simp add: Rep_mult_matrix) |
1574 done |
1621 done |
1575 |
1622 |
1576 lemma apply_matrix_add: "! x y. f (x+y) = (f x) + (f y) \<Longrightarrow> f 0 = (0::'a) \<Longrightarrow> apply_matrix f ((a::('a::lordered_ab_group_add) matrix) + b) = (apply_matrix f a) + (apply_matrix f b)" |
1623 lemma apply_matrix_add: "! x y. f (x+y) = (f x) + (f y) \<Longrightarrow> f 0 = (0::'a) |
|
1624 \<Longrightarrow> apply_matrix f ((a::('a::monoid_add) matrix) + b) = (apply_matrix f a) + (apply_matrix f b)" |
1577 apply (subst Rep_matrix_inject[symmetric]) |
1625 apply (subst Rep_matrix_inject[symmetric]) |
1578 apply (rule ext)+ |
1626 apply (rule ext)+ |
1579 apply (simp) |
1627 apply (simp) |
1580 done |
1628 done |
1581 |
1629 |
1582 lemma singleton_matrix_add: "singleton_matrix j i ((a::_::lordered_ab_group_add)+b) = (singleton_matrix j i a) + (singleton_matrix j i b)" |
1630 lemma singleton_matrix_add: "singleton_matrix j i ((a::_::monoid_add)+b) = (singleton_matrix j i a) + (singleton_matrix j i b)" |
1583 apply (subst Rep_matrix_inject[symmetric]) |
1631 apply (subst Rep_matrix_inject[symmetric]) |
1584 apply (rule ext)+ |
1632 apply (rule ext)+ |
1585 apply (simp) |
1633 apply (simp) |
1586 done |
1634 done |
1587 |
1635 |
1588 lemma nrows_mult: "nrows ((A::('a::lordered_ring) matrix) * B) <= nrows A" |
1636 lemma nrows_mult: "nrows ((A::('a::ring) matrix) * B) <= nrows A" |
1589 by (simp add: times_matrix_def mult_nrows) |
1637 by (simp add: times_matrix_def mult_nrows) |
1590 |
1638 |
1591 lemma ncols_mult: "ncols ((A::('a::lordered_ring) matrix) * B) <= ncols B" |
1639 lemma ncols_mult: "ncols ((A::('a::ring) matrix) * B) <= ncols B" |
1592 by (simp add: times_matrix_def mult_ncols) |
1640 by (simp add: times_matrix_def mult_ncols) |
1593 |
1641 |
1594 definition |
1642 definition |
1595 one_matrix :: "nat \<Rightarrow> ('a::{zero,one}) matrix" where |
1643 one_matrix :: "nat \<Rightarrow> ('a::{zero,one}) matrix" where |
1596 "one_matrix n = Abs_matrix (% j i. if j = i & j < n then 1 else 0)" |
1644 "one_matrix n = Abs_matrix (% j i. if j = i & j < n then 1 else 0)" |
1613 have "?r <= n" by (simp add: ncols_le) |
1661 have "?r <= n" by (simp add: ncols_le) |
1614 moreover have "n <= ?r" by (simp add: le_ncols, arith) |
1662 moreover have "n <= ?r" by (simp add: le_ncols, arith) |
1615 ultimately show "?r = n" by simp |
1663 ultimately show "?r = n" by simp |
1616 qed |
1664 qed |
1617 |
1665 |
1618 lemma one_matrix_mult_right[simp]: "ncols A <= n \<Longrightarrow> (A::('a::{lordered_ring,ring_1}) matrix) * (one_matrix n) = A" |
1666 lemma one_matrix_mult_right[simp]: "ncols A <= n \<Longrightarrow> (A::('a::{ring_1}) matrix) * (one_matrix n) = A" |
1619 apply (subst Rep_matrix_inject[THEN sym]) |
1667 apply (subst Rep_matrix_inject[THEN sym]) |
1620 apply (rule ext)+ |
1668 apply (rule ext)+ |
1621 apply (simp add: times_matrix_def Rep_mult_matrix) |
1669 apply (simp add: times_matrix_def Rep_mult_matrix) |
1622 apply (rule_tac j1="xa" in ssubst[OF foldseq_almostzero]) |
1670 apply (rule_tac j1="xa" in ssubst[OF foldseq_almostzero]) |
1623 apply (simp_all) |
1671 apply (simp_all) |
1624 by (simp add: max_def ncols) |
1672 by (simp add: max_def ncols) |
1625 |
1673 |
1626 lemma one_matrix_mult_left[simp]: "nrows A <= n \<Longrightarrow> (one_matrix n) * A = (A::('a::{lordered_ring, ring_1}) matrix)" |
1674 lemma one_matrix_mult_left[simp]: "nrows A <= n \<Longrightarrow> (one_matrix n) * A = (A::('a::ring_1) matrix)" |
1627 apply (subst Rep_matrix_inject[THEN sym]) |
1675 apply (subst Rep_matrix_inject[THEN sym]) |
1628 apply (rule ext)+ |
1676 apply (rule ext)+ |
1629 apply (simp add: times_matrix_def Rep_mult_matrix) |
1677 apply (simp add: times_matrix_def Rep_mult_matrix) |
1630 apply (rule_tac j1="x" in ssubst[OF foldseq_almostzero]) |
1678 apply (rule_tac j1="x" in ssubst[OF foldseq_almostzero]) |
1631 apply (simp_all) |
1679 apply (simp_all) |
1632 by (simp add: max_def nrows) |
1680 by (simp add: max_def nrows) |
1633 |
1681 |
1634 lemma transpose_matrix_mult: "transpose_matrix ((A::('a::{lordered_ring,comm_ring}) matrix)*B) = (transpose_matrix B) * (transpose_matrix A)" |
1682 lemma transpose_matrix_mult: "transpose_matrix ((A::('a::comm_ring) matrix)*B) = (transpose_matrix B) * (transpose_matrix A)" |
1635 apply (simp add: times_matrix_def) |
1683 apply (simp add: times_matrix_def) |
1636 apply (subst transpose_mult_matrix) |
1684 apply (subst transpose_mult_matrix) |
1637 apply (simp_all add: mult_commute) |
1685 apply (simp_all add: mult_commute) |
1638 done |
1686 done |
1639 |
1687 |
1640 lemma transpose_matrix_add: "transpose_matrix ((A::('a::lordered_ab_group_add) matrix)+B) = transpose_matrix A + transpose_matrix B" |
1688 lemma transpose_matrix_add: "transpose_matrix ((A::('a::monoid_add) matrix)+B) = transpose_matrix A + transpose_matrix B" |
1641 by (simp add: plus_matrix_def transpose_combine_matrix) |
1689 by (simp add: plus_matrix_def transpose_combine_matrix) |
1642 |
1690 |
1643 lemma transpose_matrix_diff: "transpose_matrix ((A::('a::lordered_ab_group_add) matrix)-B) = transpose_matrix A - transpose_matrix B" |
1691 lemma transpose_matrix_diff: "transpose_matrix ((A::('a::group_add) matrix)-B) = transpose_matrix A - transpose_matrix B" |
1644 by (simp add: diff_matrix_def transpose_combine_matrix) |
1692 by (simp add: diff_matrix_def transpose_combine_matrix) |
1645 |
1693 |
1646 lemma transpose_matrix_minus: "transpose_matrix (-(A::('a::lordered_ring) matrix)) = - transpose_matrix (A::('a::lordered_ring) matrix)" |
1694 lemma transpose_matrix_minus: "transpose_matrix (-(A::('a::group_add) matrix)) = - transpose_matrix (A::'a matrix)" |
1647 by (simp add: minus_matrix_def transpose_apply_matrix) |
1695 by (simp add: minus_matrix_def transpose_apply_matrix) |
1648 |
1696 |
1649 constdefs |
1697 constdefs |
1650 right_inverse_matrix :: "('a::{lordered_ring, ring_1}) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool" |
1698 right_inverse_matrix :: "('a::{ring_1}) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool" |
1651 "right_inverse_matrix A X == (A * X = one_matrix (max (nrows A) (ncols X))) \<and> nrows X \<le> ncols A" |
1699 "right_inverse_matrix A X == (A * X = one_matrix (max (nrows A) (ncols X))) \<and> nrows X \<le> ncols A" |
1652 left_inverse_matrix :: "('a::{lordered_ring, ring_1}) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool" |
1700 left_inverse_matrix :: "('a::{ring_1}) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool" |
1653 "left_inverse_matrix A X == (X * A = one_matrix (max(nrows X) (ncols A))) \<and> ncols X \<le> nrows A" |
1701 "left_inverse_matrix A X == (X * A = one_matrix (max(nrows X) (ncols A))) \<and> ncols X \<le> nrows A" |
1654 inverse_matrix :: "('a::{lordered_ring, ring_1}) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool" |
1702 inverse_matrix :: "('a::{ring_1}) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool" |
1655 "inverse_matrix A X == (right_inverse_matrix A X) \<and> (left_inverse_matrix A X)" |
1703 "inverse_matrix A X == (right_inverse_matrix A X) \<and> (left_inverse_matrix A X)" |
1656 |
1704 |
1657 lemma right_inverse_matrix_dim: "right_inverse_matrix A X \<Longrightarrow> nrows A = ncols X" |
1705 lemma right_inverse_matrix_dim: "right_inverse_matrix A X \<Longrightarrow> nrows A = ncols X" |
1658 apply (insert ncols_mult[of A X], insert nrows_mult[of A X]) |
1706 apply (insert ncols_mult[of A X], insert nrows_mult[of A X]) |
1659 by (simp add: right_inverse_matrix_def) |
1707 by (simp add: right_inverse_matrix_def) |
1697 apply (subst Rep_matrix_inject[symmetric]) |
1745 apply (subst Rep_matrix_inject[symmetric]) |
1698 apply (rule ext)+ |
1746 apply (rule ext)+ |
1699 apply (auto simp add: Rep_matrix_mult foldseq_zero zero_imp_mult_zero) |
1747 apply (auto simp add: Rep_matrix_mult foldseq_zero zero_imp_mult_zero) |
1700 done |
1748 done |
1701 |
1749 |
1702 lemma add_nrows: "nrows (A::('a::comm_monoid_add) matrix) <= u \<Longrightarrow> nrows B <= u \<Longrightarrow> nrows (A + B) <= u" |
1750 lemma add_nrows: "nrows (A::('a::monoid_add) matrix) <= u \<Longrightarrow> nrows B <= u \<Longrightarrow> nrows (A + B) <= u" |
1703 apply (simp add: plus_matrix_def) |
1751 apply (simp add: plus_matrix_def) |
1704 apply (rule combine_nrows) |
1752 apply (rule combine_nrows) |
1705 apply (simp_all) |
1753 apply (simp_all) |
1706 done |
1754 done |
1707 |
1755 |
1708 lemma move_matrix_row_mult: "move_matrix ((A::('a::lordered_ring) matrix) * B) j 0 = (move_matrix A j 0) * B" |
1756 lemma move_matrix_row_mult: "move_matrix ((A::('a::ring) matrix) * B) j 0 = (move_matrix A j 0) * B" |
1709 apply (subst Rep_matrix_inject[symmetric]) |
1757 apply (subst Rep_matrix_inject[symmetric]) |
1710 apply (rule ext)+ |
1758 apply (rule ext)+ |
1711 apply (auto simp add: Rep_matrix_mult foldseq_zero) |
1759 apply (auto simp add: Rep_matrix_mult foldseq_zero) |
1712 apply (rule_tac foldseq_zerotail[symmetric]) |
1760 apply (rule_tac foldseq_zerotail[symmetric]) |
1713 apply (auto simp add: nrows zero_imp_mult_zero max2) |
1761 apply (auto simp add: nrows zero_imp_mult_zero max2) |
1714 apply (rule order_trans) |
1762 apply (rule order_trans) |
1715 apply (rule ncols_move_matrix_le) |
1763 apply (rule ncols_move_matrix_le) |
1716 apply (simp add: max1) |
1764 apply (simp add: max1) |
1717 done |
1765 done |
1718 |
1766 |
1719 lemma move_matrix_col_mult: "move_matrix ((A::('a::lordered_ring) matrix) * B) 0 i = A * (move_matrix B 0 i)" |
1767 lemma move_matrix_col_mult: "move_matrix ((A::('a::ring) matrix) * B) 0 i = A * (move_matrix B 0 i)" |
1720 apply (subst Rep_matrix_inject[symmetric]) |
1768 apply (subst Rep_matrix_inject[symmetric]) |
1721 apply (rule ext)+ |
1769 apply (rule ext)+ |
1722 apply (auto simp add: Rep_matrix_mult foldseq_zero) |
1770 apply (auto simp add: Rep_matrix_mult foldseq_zero) |
1723 apply (rule_tac foldseq_zerotail[symmetric]) |
1771 apply (rule_tac foldseq_zerotail[symmetric]) |
1724 apply (auto simp add: ncols zero_imp_mult_zero max1) |
1772 apply (auto simp add: ncols zero_imp_mult_zero max1) |
1725 apply (rule order_trans) |
1773 apply (rule order_trans) |
1726 apply (rule nrows_move_matrix_le) |
1774 apply (rule nrows_move_matrix_le) |
1727 apply (simp add: max2) |
1775 apply (simp add: max2) |
1728 done |
1776 done |
1729 |
1777 |
1730 lemma move_matrix_add: "((move_matrix (A + B) j i)::(('a::lordered_ab_group_add) matrix)) = (move_matrix A j i) + (move_matrix B j i)" |
1778 lemma move_matrix_add: "((move_matrix (A + B) j i)::(('a::monoid_add) matrix)) = (move_matrix A j i) + (move_matrix B j i)" |
1731 apply (subst Rep_matrix_inject[symmetric]) |
1779 apply (subst Rep_matrix_inject[symmetric]) |
1732 apply (rule ext)+ |
1780 apply (rule ext)+ |
1733 apply (simp) |
1781 apply (simp) |
1734 done |
1782 done |
1735 |
1783 |
1736 lemma move_matrix_mult: "move_matrix ((A::('a::lordered_ring) matrix)*B) j i = (move_matrix A j 0) * (move_matrix B 0 i)" |
1784 lemma move_matrix_mult: "move_matrix ((A::('a::ring) matrix)*B) j i = (move_matrix A j 0) * (move_matrix B 0 i)" |
1737 by (simp add: move_matrix_ortho[of "A*B"] move_matrix_col_mult move_matrix_row_mult) |
1785 by (simp add: move_matrix_ortho[of "A*B"] move_matrix_col_mult move_matrix_row_mult) |
1738 |
1786 |
1739 constdefs |
1787 constdefs |
1740 scalar_mult :: "('a::lordered_ring) \<Rightarrow> 'a matrix \<Rightarrow> 'a matrix" |
1788 scalar_mult :: "('a::ring) \<Rightarrow> 'a matrix \<Rightarrow> 'a matrix" |
1741 "scalar_mult a m == apply_matrix (op * a) m" |
1789 "scalar_mult a m == apply_matrix (op * a) m" |
1742 |
1790 |
1743 lemma scalar_mult_zero[simp]: "scalar_mult y 0 = 0" |
1791 lemma scalar_mult_zero[simp]: "scalar_mult y 0 = 0" |
1744 by (simp add: scalar_mult_def) |
1792 by (simp add: scalar_mult_def) |
1745 |
1793 |