logo

Theorems (or conjectures) for the theory of proveit.linear_algebra.matrices

In [1]:
import proveit
# Prepare this notebook for defining the theorems of a theory:
%theorems_notebook # Keep this at the top following 'import proveit'.

from proveit import (a, b, b_of_j, b_of_k, c, d, f, g, i, j, k, m, n, t,
                     x, y, z, fj, gj, fy, A, P, U, V, W, S, alpha, beta)
from proveit import Function, ExprRange, IndexedVar
from proveit.core_expr_types import (bj, a_1_to_m, x_1_to_i, x_1_to_m,
                                     y_1_to_j, z_1_to_k, z_1_to_n)
from proveit.core_expr_types import (
    a_1_to_i, b_1_to_j, c_1_to_j, c_1_to_k, d_1_to_k)
from proveit.logic import Equals, Forall, Implies, Iff, InSet, InClass, SubsetEq
from proveit.numbers import Add, Mult, Exp, Sum
from proveit.numbers import one
from proveit.numbers import (Integer, Interval, Natural, NaturalPos,
                             Rational, Real, Complex)
from proveit.linear_algebra import (
    VecSpaces, LinMap, ScalarMult, MatrixSpace,
    TensorProd, MatrixMult, Unitary, SpecialUnitary)
In [2]:
%begin theorems
Defining theorems for theory 'proveit.linear_algebra.matrices'
Subsequent end-of-cell assignments will define theorems
'%end theorems' will finalize the definitions

Matrix spaces on number fields are vector spaces

In [3]:
rational_matrix_space_is_vec_space = Forall(
    (m, n), InClass(MatrixSpace(Rational, m, n),
                    VecSpaces(Rational)),
    domain=NaturalPos)
Out[3]:
rational_matrix_space_is_vec_space (conjecture without proof):

In [4]:
real_matrix_space_is_vec_space = Forall(
    (m, n), InClass(MatrixSpace(Real, m, n),
                    VecSpaces(Real)),
    domain=NaturalPos)
Out[4]:
real_matrix_space_is_vec_space (conjecture without proof):

In [5]:
complex_matrix_space_is_vec_space = Forall(
    (m, n), InClass(MatrixSpace(Complex, m, n),
                    VecSpaces(Complex)),
    domain=NaturalPos)
Out[5]:
complex_matrix_space_is_vec_space (conjecture without proof):

In [6]:
eigen_pow = (
    Forall(k,
    Forall(b,
    Forall((A, x), 
        Implies(Equals(MatrixMult(A, x), ScalarMult(b, x)), 
                Equals(MatrixMult(Exp(A, k), x), ScalarMult(Exp(b, k), x)))),
    domain=Complex), domain=NaturalPos))
Out[6]:
eigen_pow (conjecture without proof):

In [7]:
unitaries_are_matrices = Forall(
    n, SubsetEq(Unitary(n), MatrixSpace(Complex, n, n)),
    domain=NaturalPos)
Out[7]:
unitaries_are_matrices (conjecture without proof):

In [8]:
special_unitaries_are_matrices = Forall(
    n, SubsetEq(SpecialUnitary(n), MatrixSpace(Complex, n, n)),
    domain=NaturalPos)
Out[8]:
special_unitaries_are_matrices (conjecture without proof):

In [9]:
%end theorems
These theorems may now be imported from the theory package: proveit.linear_algebra.matrices